Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | start RTL -> BTL | Sylvain Boulmé | 2021-05-06 | 1 | -0/+50 |
* | clean deprecated comments | Sylvain Boulmé | 2021-05-05 | 1 | -6/+1 |
* | Factorize as suggested for call/tailcall | Léo Gourdin | 2021-05-04 | 1 | -43/+43 |
* | finishing proofs and cleanup | Léo Gourdin | 2021-05-04 | 1 | -134/+48 |
* | some advance and simplifications | Léo Gourdin | 2021-05-04 | 1 | -67/+71 |
* | suggestions... | Sylvain Boulmé | 2021-05-04 | 1 | -20/+70 |
* | builtin case OK, call and tailcall started but not finished | Léo Gourdin | 2021-05-04 | 1 | -1/+29 |
* | one example case on main proof | Léo Gourdin | 2021-05-04 | 1 | -18/+20 |
* | Some try in step_simulation | Léo Gourdin | 2021-05-04 | 1 | -3/+20 |
* | proof for Icond in iblock_istep | Léo Gourdin | 2021-05-04 | 1 | -1/+31 |
* | essai avec le cond_star_step | Sylvain Boulmé | 2021-05-04 | 1 | -12/+45 |
* | essais | Sylvain Boulmé | 2021-05-03 | 1 | -16/+31 |
* | some advance | Léo Gourdin | 2021-05-03 | 1 | -8/+39 |
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int... | Sylvain Boulmé | 2021-05-03 | 1 | -35/+22 |
|\ | |||||
| * | A better structure for inductive prop | Léo Gourdin | 2021-05-03 | 1 | -35/+25 |
* | | une autre suggestion | Sylvain Boulmé | 2021-05-03 | 1 | -0/+14 |
|/ | |||||
* | Trying a inductive predicate for BTL-RTL proof | Léo Gourdin | 2021-05-03 | 1 | -10/+41 |
* | debroussaillage et precisions... | Sylvain Boulmé | 2021-05-01 | 1 | -8/+58 |
* | BTLtoRTL: proof for internal/external/return states | Léo Gourdin | 2021-04-30 | 1 | -0/+25 |
* | start the new "BTL" IR. | Sylvain Boulmé | 2021-04-28 | 1 | -0/+127 |