| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | begin adapting for LICM phase | David Monniaux | 2020-04-01 | 2 | -32/+32 |
| * | adapting new stuff for ARM and AArch64 | David Monniaux | 2020-04-01 | 2 | -18/+14 |
| * | now able to inject on Call | David Monniaux | 2020-04-01 | 2 | -19/+16 |
| * | preparatory work for allowing injection after calls | David Monniaux | 2020-04-01 | 1 | -6/+40 |
| * | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm | David Monniaux | 2020-03-31 | 2 | -26/+29 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3 | David Monniaux | 2020-03-31 | 1 | -25/+25 |
| | |\ | |||||
| | | * | forgot an 'Admitted' | David Monniaux | 2020-03-31 | 1 | -1/+1 |
| | | * | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-03-31 | 2 | -10/+17 |
| | | |\ | |||||
| | | * \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-03-11 | 5 | -128/+366 |
| | | |\ \ | |||||
| | | * | | | same version as in dm-cse2 | David Monniaux | 2020-03-03 | 1 | -24/+24 |
| | * | | | | Merge branch 'mppa-cse3' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-31 | 2 | -0/+292 |
| | |\ \ \ \ | |||||
| | * | | | | | no more admitted | David Monniaux | 2020-03-31 | 1 | -1/+4 |
| * | | | | | | 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 | 2 | -3/+9 |
| * | | | | | | 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 | 2 | -1/+8 |
| * | | | | | | 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 | 2 | -16/+118 |
| * | | | | | | additional checks | David Monniaux | 2020-03-30 | 1 | -1/+11 |
| * | | | | | | more proofs on injector | David Monniaux | 2020-03-30 | 1 | -1/+173 |
| * | | | | | | injector wrapper function | David Monniaux | 2020-03-30 | 1 | -0/+22 |
| * | | | | | | use inject_l | David Monniaux | 2020-03-30 | 2 | -18/+10 |
| * | | | | | | 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 |
| * | | | | | | more on injection | David Monniaux | 2020-03-30 | 1 | -0/+10 |
| * | | | | | | more on injection | David Monniaux | 2020-03-30 | 1 | -2/+4 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |