Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | proof OK for Call and Return states | Léo Gourdin | 2021-05-07 | 1 | -6/+21 |
* | starting RTL->BTL proof | Léo Gourdin | 2021-05-06 | 1 | -4/+46 |
* | fix match_states | Sylvain Boulmé | 2021-05-06 | 1 | -6/+8 |
* | cleaner match_states | Sylvain Boulmé | 2021-05-06 | 1 | -16/+21 |
* | start RTL -> BTL | Sylvain Boulmé | 2021-05-06 | 5 | -50/+383 |
* | finish verify_block and proof | Léo Gourdin | 2021-05-05 | 1 | -21/+123 |
* | advance in cfg checker | Léo Gourdin | 2021-05-05 | 1 | -1/+138 |
* | 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 |
* | more implem notes in BTLroadmap | Sylvain Boulmé | 2021-05-02 | 1 | -1/+8 |
* | BTL roadmap | Sylvain Boulmé | 2021-05-02 | 1 | -0/+79 |
* | debroussaillage et precisions... | Sylvain Boulmé | 2021-05-01 | 2 | -23/+73 |
* | BTLtoRTL: proof for internal/external/return states | Léo Gourdin | 2021-04-30 | 2 | -2/+27 |
* | start the new "BTL" IR. | Sylvain Boulmé | 2021-04-28 | 6 | -2/+735 |
* | add auxfile | David Monniaux | 2021-04-27 | 1 | -0/+17 |
* | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | Léo Gourdin | 2021-04-22 | 18 | -566/+370 |
|\ | |||||
| * | fix broken link in index-kvx.html | Sylvain Boulmé | 2021-04-16 | 1 | -1/+1 |
| * | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVX | Cyril SIX | 2021-04-13 | 5 | -525/+173 |
| |\ | |||||
| | * | Cleaning | Cyril SIX | 2021-04-02 | 1 | -2/+1 |
| | * | More efficient | Cyril SIX | 2021-04-02 | 1 | -8/+12 |
| | * | Outermost loop detection works | Cyril SIX | 2021-04-02 | 1 | -9/+10 |
| | * | Getting all loop bodies | Cyril SIX | 2021-04-02 | 2 | -2/+50 |
| | * | get_loop_headers simplification (using the new get_loop_backedges) | Cyril SIX | 2021-04-02 | 1 | -39/+7 |
| | * | Simple backedge detection (modified code from get_loop_headers) | Cyril SIX | 2021-04-02 | 3 | -0/+57 |
| | * | Big simplification of get_loop_info | Cyril SIX | 2021-03-31 | 1 | -111/+16 |
| | * | Simplification of the Linearize heuristic (same result functionally) | Cyril SIX | 2021-03-30 | 1 | -216/+6 |
| | * | Simplifications on Linearize - details below | Cyril SIX | 2021-03-29 | 1 | -205/+79 |
| | * | Code simplification of get_path_map (no functionality change) | Cyril SIX | 2021-01-26 | 1 | -14/+16 |
| * | | Adding more precise heuristic measures | Cyril SIX | 2021-04-13 | 1 | -2/+62 |
| * | | Adding overpredicts | Cyril SIX | 2021-04-13 | 1 | -3/+6 |
| * | | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flag | Cyril SIX | 2021-04-13 | 1 | -33/+93 |
| * | | Adding distinction between kvx-cos and kvx-mbr (for trapping loads) | Cyril SIX | 2021-04-13 | 7 | -4/+22 |
| * | | rm spurious files | David Monniaux | 2021-04-12 | 39 | -1705/+0 |
| * | | test profiling | David Monniaux | 2021-04-12 | 42 | -0/+1720 |
| * | | collision of registers | David Monniaux | 2021-04-12 | 2 | -3/+3 |
* | | | moving my tests | Léo Gourdin | 2021-04-22 | 26 | -157/+0 |
|/ / |