| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |