aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE3proof.v
Commit message (Expand)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
|\
| * 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-09 03:08:47 +0000