Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |