| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge branch 'kvx-work-velus' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/C...patched_for_velus | David Monniaux | 2021-04-27 | 1 | -1/+1 |
| |\ | |||||
| | * | fix 64-bit | David Monniaux | 2021-04-27 | 1 | -1/+1 |
| * | | fix 4 | David Monniaux | 2021-04-27 | 1 | -1/+1 |
| |/ | |||||
| * | fix pour ARM | David Monniaux | 2021-04-27 | 1 | -1/+2 |
| * | Merge branch 'kvx-work-velus' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/C... | David Monniaux | 2021-04-27 | 15 | -227/+456 |
| |\ | |||||
| | * | disable builds that don't work | David Monniaux | 2021-04-19 | 1 | -84/+84 |
| | * | Merge remote-tracking branch 'origin/kvx-work' into kvx-work-velus | David Monniaux | 2021-04-19 | 386 | -11069/+41602 |
| | |\ | |||||
| | * \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-work-velus | David Monniaux | 2020-09-18 | 18 | -255/+290 |
| | |\ \ | |||||
| | * | | | keep Velus happy | David Monniaux | 2020-07-29 | 1 | -0/+20 |
| | * | | | fix stacklayout for velus | David Monniaux | 2020-07-28 | 1 | -1/+1 |
| | * | | | rm 'range' causing compilation to end | David Monniaux | 2020-07-28 | 1 | -1/+1 |
| | * | | | applied the Velus patch | David Monniaux | 2020-07-28 | 2 | -1/+2 |
| | * | | | Merge branch 'v3.7-velus' of github.com:inria-parkas/CompCert into kvx-work-v... | David Monniaux | 2020-07-28 | 11 | -140/+368 |
| | |\ \ \ | |||||
| | | * \ \ | Merge pull request #1 from Lionel-Rieg/v3.7-velus | Timothy Bourke | 2020-04-21 | 307 | -7791/+28881 |
| | | |\ \ \ | |||||
| | | | * | | | More rewriting for Separation | Timothy Bourke | 2020-04-21 | 1 | -14/+34 |
| | | | * | | | Fix rebase of Stackingproof/elab_char_constant | Timothy Bourke | 2020-04-21 | 3 | -10/+6 |
| | | | * | | | Fix other stacking proofs for range' | Timothy Bourke | 2020-04-21 | 2 | -2/+2 |
| | | | * | | | Rewrites in disjoint_footprint | Timothy Bourke | 2020-04-21 | 1 | -0/+15 |
| | | | * | | | Fix out-of-date comment about function allocs | Timothy Bourke | 2020-04-21 | 1 | -4/+2 |
| | | | * | | | Generalize definition of range | Timothy Bourke | 2020-04-21 | 2 | -105/+108 |
| | | | * | | | Streamline range weakening lemma | Timothy Bourke | 2020-04-21 | 1 | -13/+13 |
| | | | * | | | Add range_w for writeable static variables | Timothy Bourke | 2020-04-21 | 2 | -74/+119 |
| | | | * | | | Minor typo in docs: RTLtyping -> Ctyping | Timothy Bourke | 2020-04-21 | 1 | -1/+2 |
| | | | * | | | Expose the kind of elaborated char constants | Timothy Bourke | 2020-04-21 | 2 | -5/+5 |
| | | | * | | | Expose constant elaboration functions | Timothy Bourke | 2020-04-21 | 1 | -0/+4 |
| | | | * | | | pretty printer for Clight | Lélio Brun | 2020-04-21 | 2 | -7/+3 |
| | | | * | | | Some more separation lemmas | Timothy Bourke | 2020-04-21 | 1 | -0/+90 |
| | | | * | | | Strengthen contains massert | Timothy Bourke | 2020-04-21 | 1 | -27/+50 |
| | | | * | | | Remove unnecessary module paths | Timothy Bourke | 2020-04-21 | 1 | -0/+20 |
| | | | * | | | Semantics parametrized by function entry | Lélio Brun | 2020-04-21 | 1 | -36/+53 |
| * | | | | | | 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 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |