| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | fix for jump tablesv3.5_k1c_1.0 | David Monniaux | 2019-03-30 | 1 | -14/+18 |
| * | Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptable | Cyril SIX | 2019-03-29 | 1 | -2/+5 |
| |\ | |||||
| | * | Finition de la preuve de Asmblockgenproof | Cyril SIX | 2019-03-29 | 1 | -2/+5 |
| * | | Preuve de Jumptable dans Asmblockdeps.v | Cyril SIX | 2019-03-29 | 2 | -1/+24 |
| * | | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptable | Cyril SIX | 2019-03-29 | 7 | -23/+1120 |
| |\ \ | |/ |/| | |||||
| | * | No more Admitted | Cyril SIX | 2019-03-29 | 1 | -55/+102 |
| | * | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass | David Monniaux | 2019-03-28 | 9 | -74/+1071 |
| | |\ | |||||
| | | * | Merge branch 'mppa_vliw_essai_sylvain' of gricad-gitlab.univ-grenoble-alpes.f... | Sylvain Boulmé | 2019-03-27 | 2 | -67/+80 |
| | | |\ | |||||
| | | | * | Proof of the entire forward simulation (still stuck to do + permutations) | Cyril SIX | 2019-03-27 | 1 | -3/+10 |
| | | | * | Preuve du forward_simu du parexec_wio_bblock_aux | Cyril SIX | 2019-03-27 | 2 | -60/+70 |
| | | * | | dealing with permutations | Sylvain Boulmé | 2019-03-27 | 2 | -29/+100 |
| | | |/ | |||||
| | | * | Avancement dans Asmblockdeps.v | Cyril SIX | 2019-03-27 | 2 | -91/+113 |
| | | * | 1 coup de pouce ! | Sylvain Boulmé | 2019-03-26 | 1 | -9/+29 |
| | | * | Un peu d'avancement | Cyril SIX | 2019-03-26 | 2 | -4/+287 |
| | | * | slight simplification | Sylvain Boulmé | 2019-03-23 | 1 | -5/+4 |
| | | * | Avancement dans la preuve des bundles | Cyril SIX | 2019-03-22 | 1 | -3/+51 |
| | | * | fix for Coq.8.8 ?? | Sylvain Boulmé | 2019-03-22 | 2 | -4/+3 |
| | | * | Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu... | Cyril SIX | 2019-03-22 | 2 | -1/+72 |
| | | * | simplification of the proof | Sylvain Boulmé | 2019-03-21 | 2 | -29/+70 |
| | | * | yet another step backward | Sylvain Boulmé | 2019-03-20 | 1 | -18/+39 |
| | | * | one step further... | Sylvain Boulmé | 2019-03-20 | 1 | -6/+28 |
| | | * | premier decoupage | Sylvain Boulmé | 2019-03-20 | 1 | -2/+56 |
| | | * | Integrating Asmvliw.v in the proof chain | Cyril SIX | 2019-03-20 | 3 | -16/+29 |
| | | * | Idée de preuve VLIW | Cyril SIX | 2019-03-18 | 1 | -2/+21 |
| | | * | fix the step_internal of Asmvliw | Sylvain Boulmé | 2019-03-14 | 1 | -19/+23 |
| | | * | definition of VLIW semantics | Sylvain Boulmé | 2019-03-14 | 3 | -14/+342 |
| | * | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd) | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| * | | | Avancement dans la preuve du MBjumptable | Cyril SIX | 2019-03-29 | 1 | -1/+21 |
| * | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd) | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| * | | | Merge branch 'mppa-mul' into mppa-jumptable | David Monniaux | 2019-03-22 | 14 | -719/+123 |
| |\ \ \ | |||||
| | * \ \ | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-22 | 13 | -783/+14 |
| | |\ \ \ | |||||
| | | * | | | rm Pdiv / Pdivu | David Monniaux | 2019-03-22 | 6 | -66/+1 |
| | | * | | | restructuration pour compilation toute archi | David Monniaux | 2019-03-22 | 3 | -1/+5 |
| | | * | | | ça recompile sur x86 | David Monniaux | 2019-03-22 | 2 | -103/+1 |
| | | * | | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-22 | 3 | -613/+7 |
| | | |\| | | |||||
| | | | * | | I think it should now compile for all architectures. | David Monniaux | 2019-03-22 | 1 | -613/+0 |
| | | | * | | try to be portable across archs | David Monniaux | 2019-03-21 | 2 | -0/+7 |
| | * | | | | rm tests inherited from Risc-V | David Monniaux | 2019-03-20 | 1 | -30/+5 |
| | |/ / / | |||||
| | * | | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-20 | 1 | -2/+2 |
| | |\| | | |||||
| | * | | | Proof of div32/mod32/divf32/divf64 lemmas | Cyril SIX | 2019-03-20 | 1 | -6/+21 |
| | * | | | la division flottante fonctionne | David Monniaux | 2019-03-20 | 2 | -2/+27 |
| | * | | | begin float division | David Monniaux | 2019-03-20 | 1 | -0/+4 |
| | * | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-20 | 1 | -6/+47 |
| | |\ \ \ | |||||
| | | * | | | Proving eval_divs_base | Cyril SIX | 2019-03-20 | 1 | -6/+47 |
| | * | | | | les divisions entieres passent | David Monniaux | 2019-03-20 | 2 | -9/+11 |
| | * | | | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-20 | 20 | -1449/+461 |
| | |\ \ \ \ | | |/ / / | |/| | | | |||||
| | * | | | | added helper functions but strange | David Monniaux | 2019-03-19 | 3 | -5/+162 |
| * | | | | | Jump tables now work. There is still an "Admitted" subcase in a proof. | David Monniaux | 2019-03-22 | 3 | -5/+15 |
| * | | | | | on avance sur la jumptable | David Monniaux | 2019-03-22 | 2 | -3/+3 |
| * | | | | | jumptable avance | David Monniaux | 2019-03-22 | 1 | -1/+8 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |