Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'RTL_has_loaded' into kvx-work | Léo Gourdin | 2021-11-02 | 23 | -1382/+1324 |
|\ | |||||
| * | bugfix | Léo Gourdin | 2021-11-02 | 1 | -2/+2 |
| * | being more archi-independant | Léo Gourdin | 2021-11-02 | 8 | -22/+19 |
| * | Porting the BTL non-trap loads approach to RTL | Léo Gourdin | 2021-11-02 | 23 | -1377/+1322 |
* | | Merge remote-tracking branch 'origin/master' into towards_3.10 | David Monniaux | 2021-10-29 | 2 | -2/+2 |
|\ \ | |/ |/| | |||||
| * | Qualify `Instance` and `Program Instance` as `Global` | Xavier Leroy | 2021-10-03 | 2 | -2/+2 |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-24 | 2 | -5/+8 |
|\| | |||||
| * | Avoid `Global Set Asymmetric Patterns` (#408) | Xavier Leroy | 2021-09-15 | 1 | -2/+5 |
| * | Handle the new warnings of OCaml 4.13 | Xavier Leroy | 2021-09-13 | 1 | -3/+3 |
| * | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 2 | -8/+10 |
| * | Emit no entry for variables without init in json. | Bernhard Schommer | 2021-04-29 | 1 | -1/+7 |
| * | Use List.repeat from Coq's standard library instead of list_repeat | Xavier Leroy | 2021-04-19 | 1 | -1/+1 |
* | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2021-09-01 | 3 | -5/+107 |
|\ \ | |||||
| * | | cleanup | Léo Gourdin | 2021-09-01 | 1 | -9/+0 |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-work | Léo Gourdin | 2021-09-01 | 5 | -89/+24 |
| |\ \ | |||||
| * \ \ | [MERGE] BTL into kvx-work (replacing RTLpath) | Léo Gourdin | 2021-09-01 | 3 | -5/+116 |
| |\ \ \ | |||||
| | * \ \ | Merge branch 'kvx-work' into BTL | Léo Gourdin | 2021-06-10 | 38 | -738/+774 |
| | |\ \ \ | |||||
| | * | | | | [disabled checker] BTL Scheduling and Renumbering OK! | Léo Gourdin | 2021-05-27 | 1 | -0/+1 |
| | * | | | | Moving common tools, adding liveness input/output information to BTL generati... | Léo Gourdin | 2021-05-24 | 3 | -2/+39 |
| | * | | | | Changing to an opaq record in BTL info, this is a broken commit | Léo Gourdin | 2021-05-20 | 1 | -0/+52 |
| | * | | | | Grouping common RTL functions, printer improvement | Léo Gourdin | 2021-05-19 | 2 | -5/+2 |
* | | | | | | Merge remote-tracking branch 'origin/parameterized-cse3' into kvx-work | David Monniaux | 2021-09-01 | 4 | -61/+79 |
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | | | |||||
| * | | | | | more parameterization | David Monniaux | 2021-07-16 | 1 | -2/+0 |
| * | | | | | make operations cse3 parametric | David Monniaux | 2021-07-16 | 2 | -6/+10 |
| * | | | | | make trivial ops parametric | David Monniaux | 2021-07-16 | 2 | -6/+7 |
| * | | | | | make conditions a parameter in CSE3 | David Monniaux | 2021-07-16 | 2 | -3/+12 |
| * | | | | | rename parameterized versions | David Monniaux | 2021-07-16 | 2 | -38/+38 |
| * | | | | | make CSE3 condition parametric | David Monniaux | 2021-07-16 | 2 | -29/+42 |
| * | | | | | rm condition parametrization in CSE3analysis | David Monniaux | 2021-07-16 | 2 | -13/+6 |
* | | | | | | RTLTunneling: fix comments and authors information | Sylvain Boulmé | 2021-08-24 | 5 | -89/+24 |
| |/ / / / |/| | | | | |||||
* | | | | | remove default_notrap_load_value | Sylvain Boulmé | 2021-07-24 | 1 | -1/+1 |
* | | | | | Merge branch 'kvx-work' into rtl-tunneling | Sylvain Boulmé | 2021-07-24 | 13 | -25/+18 |
|\| | | | | |||||
| * | | | | Replacing default notrap load value by Vundef everywherecsix-PhD | Cyril SIX | 2021-06-18 | 13 | -25/+18 |
| | |/ / | |/| | | |||||
* | | | | Change "Tunneling" to "LTLTunneling" everywhere | Pierre Goutagny | 2021-06-17 | 5 | -5/+5 |
* | | | | Use Tunnelinglibs in Tunnelingaux | Pierre Goutagny | 2021-06-17 | 1 | -256/+81 |
* | | | | Simplify tunneling factorisation | Pierre Goutagny | 2021-06-17 | 2 | -168/+173 |
* | | | | Use Tunnelinglibs in RTLTunnelingaux | Pierre Goutagny | 2021-06-16 | 2 | -265/+123 |
* | | | | Add Tunneling factorisation module | Pierre Goutagny | 2021-06-16 | 1 | -0/+237 |
* | | | | Add RTL Tunneling as a pass | Pierre Goutagny | 2021-06-14 | 2 | -0/+6 |
* | | | | Add the RTLTunneling oracle | Pierre Goutagny | 2021-06-14 | 1 | -0/+284 |
* | | | | Complete RTLTunnelingproof | Pierre Goutagny | 2021-06-11 | 1 | -16/+66 |
* | | | | Complete `tunnel_step_correct` proof up to Ijumptable | Pierre Goutagny | 2021-06-10 | 1 | -9/+227 |
* | | | | Starts proof for `tunnel_step_correct` | Pierre Goutagny | 2021-06-09 | 1 | -15/+120 |
* | | | | Monday's work on RTLTunnelingproof | Pierre Goutagny | 2021-06-07 | 1 | -31/+153 |
* | | | | Add RTLTunnelingproof.v | Pierre Goutagny | 2021-06-04 | 1 | -0/+170 |
* | | | | Fix check_instr Icond target conditions | Pierre Goutagny | 2021-06-04 | 1 | -2/+2 |
* | | | | Write RTLTunneling.v | Pierre Goutagny | 2021-06-03 | 1 | -0/+125 |
* | | | | Add RTLTunneling.v | Pierre Goutagny | 2021-06-03 | 1 | -0/+0 |
|/ / / | |||||
* | | | Merge remote-tracking branch 'verimag/manuscript' into kvx-work | Cyril SIX | 2021-06-01 | 1 | -13/+11 |
|\ \ \ | |||||
| * | | | Do not rotate if the CB was already at the end. | Cyril SIX | 2021-04-28 | 1 | -1/+5 |