Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
* | 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 |