| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | being more archi-independant | Léo Gourdin | 2021-11-02 | 1 | -3/+3 |
| | | |||||
| * | Porting the BTL non-trap loads approach to RTL | Léo Gourdin | 2021-11-02 | 1 | -6/+14 |
| | | |||||
| * | CI fix on arm | Léo Gourdin | 2021-08-02 | 1 | -2/+2 |
| | | |||||
| * | ci fix? | Léo Gourdin | 2021-07-28 | 1 | -0/+2 |
| | | |||||
| * | non trapping loads | Léo Gourdin | 2021-07-23 | 1 | -1/+2 |
| | | |||||
| * | Fix compile on ARM/x86 backends | Léo Gourdin | 2021-07-20 | 1 | -4/+4 |
| | | |||||
| * | starting to extend RTLtoBTL with Liveness checking (on BTL side) | Sylvain Boulmé | 2021-05-28 | 1 | -0/+12 |
| | | |||||
| * | splitting BTL by introducing BTLmatchRTL | Sylvain Boulmé | 2021-05-28 | 1 | -37/+5 |
| | | | | | | reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL | ||||
| * | Merge branch 'BTL_fsem' into BTL | Léo Gourdin | 2021-05-28 | 1 | -5/+13 |
| |\ | |||||
| | * | most of the proof BTL.fsem -> BTL.cfgsem. | Sylvain Boulmé | 2021-05-28 | 1 | -2/+10 |
| | | | |||||
| | * | defines fsem (aka functional semantics) of BTL | Sylvain Boulmé | 2021-05-20 | 1 | -3/+3 |
| | | | |||||
| * | | [disabled checker] BTL Scheduling and Renumbering OK! | Léo Gourdin | 2021-05-27 | 1 | -2/+2 |
| | | | |||||
| * | | Now supporting Bnop insertion in conditions | Léo Gourdin | 2021-05-21 | 1 | -9/+20 |
| | | | |||||
| * | | Changing to an opaq record in BTL info, this is a broken commit | Léo Gourdin | 2021-05-20 | 1 | -8/+8 |
| | | | |||||
| * | | Adding a BTL record to help oracles | Léo Gourdin | 2021-05-19 | 1 | -3/+3 |
| |/ | |||||
| * | 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 ↵ | Sylvain Boulmé | 2021-05-03 | 1 | -35/+22 |
| |\ | | | | | | | into BTL | ||||
| | * | 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 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |