| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Porting the BTL non-trap loads approach to RTL | Léo Gourdin | 2021-11-02 | 1 | -125/+129 |
| * | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 1 | -4/+4 |
| * | backport to coq 8.10.2 | Sylvain Boulmé | 2020-05-11 | 1 | -4/+4 |
| * | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+12 |
| * | adapt for Icond with predicted direction | David Monniaux | 2020-04-16 | 1 | -8/+8 |
| * | begin adapting for LICM phase | David Monniaux | 2020-04-01 | 1 | -30/+30 |
| * | adapting new stuff for ARM and AArch64 | David Monniaux | 2020-04-01 | 1 | -9/+6 |
| * | now able to inject on Call | David Monniaux | 2020-04-01 | 1 | -18/+15 |
| * | preparatory work for allowing injection after calls | David Monniaux | 2020-04-01 | 1 | -6/+40 |
| * | no more admitted | David Monniaux | 2020-03-31 | 1 | -3/+5 |
| * | fewer admits | David Monniaux | 2020-03-31 | 1 | -1/+11 |
| * | resolved an "admit" | David Monniaux | 2020-03-31 | 1 | -3/+20 |
| * | more about builtin args | David Monniaux | 2020-03-31 | 1 | -1/+83 |
| * | except for builtins, finished the proof | David Monniaux | 2020-03-31 | 1 | -2/+8 |
| * | external call | David Monniaux | 2020-03-31 | 1 | -1/+8 |
| * | internal call | David Monniaux | 2020-03-31 | 1 | -1/+11 |
| * | return | David Monniaux | 2020-03-31 | 1 | -1/+29 |
| * | jumptable | David Monniaux | 2020-03-31 | 1 | -1/+22 |
| * | cond | David Monniaux | 2020-03-31 | 1 | -2/+54 |
| * | builtin (incomplete) | David Monniaux | 2020-03-31 | 1 | -0/+33 |
| * | tailcall | David Monniaux | 2020-03-31 | 1 | -1/+58 |
| * | call (could not handle it) | David Monniaux | 2020-03-31 | 1 | -1/+62 |
| * | store | David Monniaux | 2020-03-31 | 1 | -1/+42 |
| * | loads | David Monniaux | 2020-03-31 | 1 | -3/+126 |
| * | lots of admits to be filled | David Monniaux | 2020-03-31 | 1 | -13/+134 |
| * | transf_function_redirects | David Monniaux | 2020-03-31 | 1 | -0/+109 |
| * | INJnop | David Monniaux | 2020-03-31 | 1 | -1/+5 |
| * | transf_function_inj_plusstep | David Monniaux | 2020-03-31 | 1 | -0/+25 |
| * | transf_function_inj_end | David Monniaux | 2020-03-31 | 1 | -0/+57 |
| * | injector "ghost steps" | David Monniaux | 2020-03-31 | 1 | -4/+35 |
| * | one more admit | David Monniaux | 2020-03-31 | 1 | -7/+85 |
| * | lemma on stepping through non trapping instructions | David Monniaux | 2020-03-30 | 1 | -6/+100 |
| * | more proofs on injector | David Monniaux | 2020-03-30 | 1 | -1/+173 |
| * | use inject_l | David Monniaux | 2020-03-30 | 1 | -18/+3 |
| * | inject_l_redirects | David Monniaux | 2020-03-30 | 1 | -0/+82 |
| * | inject_l injected_end | David Monniaux | 2020-03-30 | 1 | -0/+90 |
| * | inject_l injected | David Monniaux | 2020-03-30 | 1 | -4/+43 |
| * | injection positions.. | David Monniaux | 2020-03-30 | 1 | -4/+49 |
| * | injection positions are ok | David Monniaux | 2020-03-30 | 1 | -0/+24 |
| * | inject_at injects the end | David Monniaux | 2020-03-30 | 1 | -5/+26 |
| * | injector injects the end | David Monniaux | 2020-03-30 | 1 | -4/+19 |
| * | injector injects.. | David Monniaux | 2020-03-30 | 1 | -0/+69 |
| * | preservation lemmas | David Monniaux | 2020-03-30 | 1 | -0/+155 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |