Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | forgot the Makefile | David Monniaux | 2019-03-10 | 1 | -0/+18 |
| | |||||
* | test for volatiles | David Monniaux | 2019-03-10 | 1 | -0/+33 |
| | |||||
* | volatile stores | David Monniaux | 2019-03-10 | 3 | -45/+42 |
| | |||||
* | volatile load | David Monniaux | 2019-03-10 | 1 | -37/+37 |
| | |||||
* | demo for volatile | David Monniaux | 2019-03-09 | 2 | -9/+28 |
| | |||||
* | program for testing volatiles | David Monniaux | 2019-03-09 | 1 | -0/+32 |
| | |||||
* | store the assembly source code as well | David Monniaux | 2019-03-09 | 1 | -5/+8 |
| | |||||
* | code qui plante | David Monniaux | 2019-03-08 | 3 | -0/+33 |
| | |||||
* | Modified test/c/Makefile for CompCert tests (remove all the float tests with ↵ | Cyril SIX | 2019-03-08 | 2 | -5/+6 |
| | | | | division) | ||||
* | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-08 | 1 | -0/+1 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | Added error message for Odivfs in Asmblockgen | Cyril SIX | 2019-03-08 | 1 | -0/+1 |
| | | |||||
* | | un example avec varargs flottants | David Monniaux | 2019-03-08 | 1 | -0/+34 |
|/ | |||||
* | disable useless warnings | David Monniaux | 2019-03-08 | 4 | -4/+4 |
| | |||||
* | Rajout de commentaires sur les instructions non émises | Cyril SIX | 2019-03-08 | 1 | -8/+8 |
| | |||||
* | Fix for the compw immediate problem | Cyril SIX | 2019-03-08 | 1 | -7/+17 |
| | |||||
* | Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types) | Cyril SIX | 2019-03-08 | 1 | -8/+8 |
| | |||||
* | Refactorisation des load et des store | Cyril SIX | 2019-03-08 | 3 | -62/+40 |
| | |||||
* | Reverting the hack introduces on Pcompw etc.. | Cyril SIX | 2019-03-08 | 1 | -14/+3 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch | Cyril SIX | 2019-03-08 | 9 | -45/+394 |
|\ | |||||
| * | Preuves du branchement avec des float | Cyril SIX | 2019-03-07 | 1 | -25/+242 |
| | | |||||
| * | Fix minor proof | Cyril SIX | 2019-03-07 | 3 | -27/+142 |
| | | |||||
| * | stop warning about system includes | David Monniaux | 2019-03-07 | 3 | -3/+3 |
| | | |||||
| * | Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2) | Cyril SIX | 2019-03-07 | 1 | -10/+14 |
| | | |||||
| * | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-07 | 1 | -2/+8 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| | * | HACK for Pcompiw/Pcompil as well | Cyril SIX | 2019-03-07 | 1 | -2/+8 |
| | | | |||||
| * | | forgot the .h | David Monniaux | 2019-03-07 | 1 | -0/+4 |
| |/ | |||||
| * | HACK for the Pcompw/Pcompl memory problem (but performance decrease, to ↵ | Cyril SIX | 2019-03-06 | 1 | -1/+4 |
| | | | | | | | | remove later) | ||||
* | | Fixing Asmblockdeps proofs | Cyril SIX | 2019-03-08 | 1 | -147/+21 |
| | | |||||
* | | Refactorized Asmblock exec_basic_instr | Cyril SIX | 2019-03-08 | 2 | -105/+121 |
| | | |||||
* | | axioms on pointer comparison removed ! | Sylvain Boulmé | 2019-03-07 | 1 | -11/+12 |
| | | |||||
* | | remove dep of exec_arith_instr on memory. | Sylvain Boulmé | 2019-03-07 | 3 | -66/+77 |
| | | | | | | | | | | | | TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible. | ||||
* | | Experiment Patch of Memory Model | Sylvain Boulmé | 2019-03-07 | 3 | -21/+48 |
|/ | |||||
* | Merge branch 'mppa_postpass' of ↵ | Sylvain Boulmé | 2019-03-06 | 3 | -3/+63 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-05 | 2 | -20/+218 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-05 | 6 | -81/+24 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-05 | 7 | -85/+187 |
| |\ \ \ | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-02 | 24 | -1377/+2286 |
| |\ \ \ \ | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-22 | 1 | -5/+131 |
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ \ \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-21 | 2 | -26/+101 |
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ \ \ \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-20 | 1 | -31/+41 |
| |\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * \ \ \ \ \ \ \ | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-02-20 | 12 | -98/+701 |
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | | | | | | | | | mul8: loop-invariant code motion | David Monniaux | 2019-02-19 | 3 | -3/+63 |
| | | | | | | | | | | |||||
* | | | | | | | | | | fix eq sur OIncremPC | Sylvain Boulmé | 2019-03-06 | 1 | -7/+14 |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||||
* | | | | | | | | | quick fix of equalities issues | Sylvain Boulmé | 2019-03-05 | 2 | -1/+10 |
| | | | | | | | | | |||||
* | | | | | | | | | Added pretty printers | Cyril SIX | 2019-03-05 | 1 | -19/+208 |
| |_|_|_|_|_|_|/ |/| | | | | | | | |||||
* | | | | | | | | fix extraction of ImpConfig | Sylvain Boulmé | 2019-03-05 | 1 | -2/+5 |
| | | | | | | | | |||||
* | | | | | | | | compilation of ImpIOOracles | Sylvain Boulmé | 2019-03-05 | 3 | -5/+9 |
| | | | | | | | | |||||
* | | | | | | | | No more axioms remaining (scheduling completely proven), however error at ↵ | Cyril SIX | 2019-03-05 | 2 | -74/+10 |
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | extraction | ||||
* | | | | | | | C'est moi qui avait fait des betises avec CoqIDE, ça remarche | Cyril SIX | 2019-03-05 | 1 | -8/+26 |
| | | | | | | | |||||
* | | | | | | | [BROKEN] error with the new is_constant and is_constant_correct | Cyril SIX | 2019-03-05 | 1 | -26/+8 |
| | | | | | | |