| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | fix some merge errors | Léo Gourdin | 2021-05-28 | 1 | -1/+1 |
| * | Merge branch 'BTL_fsem' into BTL | Léo Gourdin | 2021-05-28 | 1 | -246/+295 |
| |\ | |||||
| | * | most of the proof BTL.fsem -> BTL.cfgsem. | Sylvain Boulmé | 2021-05-28 | 1 | -1/+1 |
| | * | cleaning BTL_SEtheory | Sylvain Boulmé | 2021-05-27 | 1 | -190/+114 |
| | * | end of BTL_SEtheory w.r.t fsem | Sylvain Boulmé | 2021-05-27 | 1 | -162/+169 |
| | * | fix tr_sis definition | Sylvain Boulmé | 2021-05-26 | 1 | -57/+90 |
| | * | fix Builtin semantics | Sylvain Boulmé | 2021-05-25 | 1 | -27/+3 |
| | * | starting to experiment SE of fsem | Sylvain Boulmé | 2021-05-25 | 1 | -55/+158 |
| | * | defines fsem (aka functional semantics) of BTL | Sylvain Boulmé | 2021-05-20 | 1 | -6/+12 |
| * | | Changing to an opaq record in BTL info, this is a broken commit | Léo Gourdin | 2021-05-20 | 1 | -7/+7 |
| * | | Adding a BTL record to help oracles | Léo Gourdin | 2021-05-19 | 1 | -11/+11 |
| |/ | |||||
| * | better autodestruct ? | Sylvain Boulmé | 2021-05-11 | 1 | -16/+0 |
| * | prove sexec_exact | Sylvain Boulmé | 2021-05-11 | 1 | -11/+323 |
| * | sexec: renommage Sdead -> Sabort + simplification de sexec_correct | Sylvain Boulmé | 2021-05-08 | 1 | -57/+21 |
| * | start a model of symbolic execution in Continuation-Passing-Style | Sylvain Boulmé | 2021-05-07 | 1 | -18/+233 |
| * | fix SymbValPreserved section | Sylvain Boulmé | 2021-05-07 | 1 | -1/+98 |
| * | refactorisation + 1ere version de sstate | Sylvain Boulmé | 2021-05-06 | 1 | -1461/+169 |
| * | init BTL_SEtheory (by copy/paste from RTLpathSE_theory) | Sylvain Boulmé | 2021-05-06 | 1 | -0/+1831 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |