aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE3proof.v
Commit message (Collapse)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-214/+221
|
* make operations cse3 parametricDavid Monniaux2021-07-161-3/+3
|
* make trivial ops parametricDavid Monniaux2021-07-161-2/+2
|
* make conditions a parameter in CSE3David Monniaux2021-07-161-3/+5
|
* rename parameterized versionsDavid Monniaux2021-07-161-31/+31
|
* make CSE3 condition parametricDavid Monniaux2021-07-161-28/+31
|
* Conditions now propagated by CSE3David Monniaux2021-01-201-32/+362
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * totally switch off conditions in cse3David Monniaux2020-12-091-0/+2
| |
| * CSE3 + conditions proofDavid Monniaux2020-12-091-33/+34
| |
| * proof for jumptableDavid Monniaux2020-12-091-1/+27
| |
| * one 'admit' lessDavid Monniaux2020-12-091-2/+36
| |
| * avancement dans les preuvesDavid Monniaux2020-12-091-1/+34
| |
| * progress moving to list of itemsDavid Monniaux2020-12-091-65/+208
| |
| * analysis with Abst_sameDavid Monniaux2020-12-081-3/+9
| |
| * not yet the transfer functions that record predicatesDavid Monniaux2020-11-261-7/+54
| |
| * remains one admitDavid Monniaux2020-11-261-8/+46
| |
* | -fcse3-trivial-opsDavid Monniaux2021-01-071-2/+2
|/
* reinstated old versionDavid Monniaux2020-10-301-3/+4
|
* CSE3 trivial_ops flagDavid Monniaux2020-10-291-2/+2
|
* in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-291-2/+1
|
* centralize if_sameDavid Monniaux2020-10-091-6/+0
|
* Adding copyrightsCyril SIX2020-05-041-0/+12
|
* forward moves through CSE3 storeDavid Monniaux2020-04-211-1/+4
|
* CSE3: better builtin handlingDavid Monniaux2020-04-161-3/+5
|
* no more admittedDavid Monniaux2020-03-311-1/+4
|
* is_trivial_op in CSE3David Monniaux2020-03-141-4/+16
|
* no more 'admit' in CSE3David Monniaux2020-03-141-2/+4
|
* Iload notrapDavid Monniaux2020-03-141-2/+101
|
* IreturnDavid Monniaux2020-03-141-2/+1
|
* IreturnDavid Monniaux2020-03-141-7/+7
|
* IjumptableDavid Monniaux2020-03-141-3/+4
|
* IcondDavid Monniaux2020-03-141-3/+4
|
* ItailcallDavid Monniaux2020-03-141-3/+19
|
* IcallDavid Monniaux2020-03-141-1/+13
|
* moving forward in loadsDavid Monniaux2020-03-131-2/+52
|
* moving forward but could be simplifiedDavid Monniaux2020-03-131-26/+64
|
* CSE3 proofs: REL is inductiveDavid Monniaux2020-03-131-1/+13
|
* moving forward in proofsDavid Monniaux2020-03-131-1/+20
|
* moving forward in proofsDavid Monniaux2020-03-131-2/+35
|
* progress on inductiveness proofDavid Monniaux2020-03-131-2/+18
|
* some automationDavid Monniaux2020-03-131-29/+33
|
* some progress (but broken proof)David Monniaux2020-03-131-36/+87
|
* begin adding invariants and inductivenessDavid Monniaux2020-03-131-9/+17
|
* fmap_semDavid Monniaux2020-03-131-1/+65
|
* inductiveDavid Monniaux2020-03-131-0/+13
|
* proof sketch for CSE3 stepsDavid Monniaux2020-03-121-9/+236
|
* begin writing match states predicatesDavid Monniaux2020-03-121-27/+57
|
* inductiveness test in CSE3David Monniaux2020-03-121-1/+3
|
* removed second analysis phaseDavid Monniaux2020-03-121-0/+2
|
* typing and store stuffDavid Monniaux2020-03-121-34/+57
|
generated by cgit (git 2.34.1) at 2024-05-20 07:17:55 +0000