Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 1 | -32/+362 |
|\ | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work | ||||
| * | totally switch off conditions in cse3 | David Monniaux | 2020-12-09 | 1 | -0/+2 |
| | | |||||
| * | CSE3 + conditions proof | David Monniaux | 2020-12-09 | 1 | -33/+34 |
| | | |||||
| * | proof for jumptable | David Monniaux | 2020-12-09 | 1 | -1/+27 |
| | | |||||
| * | one 'admit' less | David Monniaux | 2020-12-09 | 1 | -2/+36 |
| | | |||||
| * | avancement dans les preuves | David Monniaux | 2020-12-09 | 1 | -1/+34 |
| | | |||||
| * | progress moving to list of items | David Monniaux | 2020-12-09 | 1 | -65/+208 |
| | | |||||
| * | analysis with Abst_same | David Monniaux | 2020-12-08 | 1 | -3/+9 |
| | | |||||
| * | not yet the transfer functions that record predicates | David Monniaux | 2020-11-26 | 1 | -7/+54 |
| | | |||||
| * | remains one admit | David Monniaux | 2020-11-26 | 1 | -8/+46 |
| | | |||||
* | | -fcse3-trivial-ops | David Monniaux | 2021-01-07 | 1 | -2/+2 |
|/ | |||||
* | reinstated old version | David Monniaux | 2020-10-30 | 1 | -3/+4 |
| | |||||
* | CSE3 trivial_ops flag | David Monniaux | 2020-10-29 | 1 | -2/+2 |
| | |||||
* | in CSE3 choose lowest variable as representative for moves | David Monniaux | 2020-10-29 | 1 | -2/+1 |
| | |||||
* | centralize if_same | David Monniaux | 2020-10-09 | 1 | -6/+0 |
| | |||||
* | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+12 |
| | |||||
* | forward moves through CSE3 store | David Monniaux | 2020-04-21 | 1 | -1/+4 |
| | |||||
* | CSE3: better builtin handling | David Monniaux | 2020-04-16 | 1 | -3/+5 |
| | |||||
* | no more admitted | David Monniaux | 2020-03-31 | 1 | -1/+4 |
| | |||||
* | is_trivial_op in CSE3 | David Monniaux | 2020-03-14 | 1 | -4/+16 |
| | |||||
* | no more 'admit' in CSE3 | David Monniaux | 2020-03-14 | 1 | -2/+4 |
| | |||||
* | Iload notrap | David Monniaux | 2020-03-14 | 1 | -2/+101 |
| | |||||
* | Ireturn | David Monniaux | 2020-03-14 | 1 | -2/+1 |
| | |||||
* | Ireturn | David Monniaux | 2020-03-14 | 1 | -7/+7 |
| | |||||
* | Ijumptable | David Monniaux | 2020-03-14 | 1 | -3/+4 |
| | |||||
* | Icond | David Monniaux | 2020-03-14 | 1 | -3/+4 |
| | |||||
* | Itailcall | David Monniaux | 2020-03-14 | 1 | -3/+19 |
| | |||||
* | Icall | David Monniaux | 2020-03-14 | 1 | -1/+13 |
| | |||||
* | moving forward in loads | David Monniaux | 2020-03-13 | 1 | -2/+52 |
| | |||||
* | moving forward but could be simplified | David Monniaux | 2020-03-13 | 1 | -26/+64 |
| | |||||
* | CSE3 proofs: REL is inductive | David Monniaux | 2020-03-13 | 1 | -1/+13 |
| | |||||
* | moving forward in proofs | David Monniaux | 2020-03-13 | 1 | -1/+20 |
| | |||||
* | moving forward in proofs | David Monniaux | 2020-03-13 | 1 | -2/+35 |
| | |||||
* | progress on inductiveness proof | David Monniaux | 2020-03-13 | 1 | -2/+18 |
| | |||||
* | some automation | David Monniaux | 2020-03-13 | 1 | -29/+33 |
| | |||||
* | some progress (but broken proof) | David Monniaux | 2020-03-13 | 1 | -36/+87 |
| | |||||
* | begin adding invariants and inductiveness | David Monniaux | 2020-03-13 | 1 | -9/+17 |
| | |||||
* | fmap_sem | David Monniaux | 2020-03-13 | 1 | -1/+65 |
| | |||||
* | inductive | David Monniaux | 2020-03-13 | 1 | -0/+13 |
| | |||||
* | proof sketch for CSE3 steps | David Monniaux | 2020-03-12 | 1 | -9/+236 |
| | |||||
* | begin writing match states predicates | David Monniaux | 2020-03-12 | 1 | -27/+57 |
| | |||||
* | inductiveness test in CSE3 | David Monniaux | 2020-03-12 | 1 | -1/+3 |
| | |||||
* | removed second analysis phase | David Monniaux | 2020-03-12 | 1 | -0/+2 |
| | |||||
* | typing and store stuff | David Monniaux | 2020-03-12 | 1 | -34/+57 |
| | |||||
* | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -0/+138 |