Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | nxor | David Monniaux | 2019-03-16 | 12 | -3/+59 |
| | |||||
* | nor implemente | David Monniaux | 2019-03-16 | 7 | -0/+39 |
| | |||||
* | partial norw | David Monniaux | 2019-03-16 | 5 | -9/+26 |
| | |||||
* | nand is implemented | David Monniaux | 2019-03-16 | 6 | -2/+28 |
| | |||||
* | some more nand | David Monniaux | 2019-03-16 | 3 | -3/+45 |
| | |||||
* | nand debut | David Monniaux | 2019-03-16 | 3 | -0/+18 |
| | |||||
* | fix problem with ALU reservation tables | David Monniaux | 2019-03-16 | 1 | -1/+3 |
| | |||||
* | 32-bit rotate finished | David Monniaux | 2019-03-16 | 6 | -6/+17 |
| | |||||
* | select rotate ops 32-bit | David Monniaux | 2019-03-16 | 3 | -2/+74 |
| | |||||
* | some more progress on rotate | David Monniaux | 2019-03-16 | 2 | -0/+6 |
| | |||||
* | ValueAOp rotate 32-bit | David Monniaux | 2019-03-16 | 1 | -0/+1 |
| | |||||
* | instruction rotate | David Monniaux | 2019-03-16 | 2 | -0/+3 |
| | |||||
* | Removing SelectLong.v from the git repo (compiled from SelectLong.vp) | Cyril SIX | 2019-03-15 | 2 | -800/+1 |
| | |||||
* | better robustness wrt exceptions | David Monniaux | 2019-03-14 | 1 | -5/+9 |
| | |||||
* | Corrigé certaines latences (Store -> 1 i/o 3, Set -> 4 i/o 3) | Cyril SIX | 2019-03-13 | 1 | -4/+3 |
| | |||||
* | Fix for CompCert 3.5 | Cyril SIX | 2019-03-13 | 1 | -0/+1 |
| | |||||
* | Enlevé la dépendance mémoire de Pcbu | Cyril SIX | 2019-03-13 | 3 | -25/+25 |
| | |||||
* | for using CPlex | David Monniaux | 2019-03-13 | 1 | -1/+12 |
| | |||||
* | Merge branch 'mppa_postpass' of ↵ | David Monniaux | 2019-03-12 | 2 | -109/+134 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass | ||||
| * | Added cascaded_scheduler but the flag does not work | Cyril SIX | 2019-03-12 | 1 | -1/+1 |
| | | |||||
| * | Added a flag for changing the scheduler (not any choice available right now) | Cyril SIX | 2019-03-12 | 1 | -2/+3 |
| | | |||||
| * | Proof of exec_trans_pcincr solved | Cyril SIX | 2019-03-12 | 1 | -7/+31 |
| | | |||||
| * | Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheck | Cyril SIX | 2019-03-12 | 1 | -12/+12 |
| |\ | |||||
| | * | fix trans_pcincr for parcheck. (Proof is broken. cf FIXME) | Sylvain Boulmé | 2019-03-12 | 1 | -12/+12 |
| | | | |||||
| * | | Simplification des preuves "de discrimination" dans Asmblockdeps | Cyril SIX | 2019-03-12 | 1 | -94/+77 |
| |/ | |||||
| * | [BROKEN] Added parallelizability check - breaks all the conditional jumps | Cyril SIX | 2019-03-12 | 2 | -1/+19 |
| | | |||||
* | | -fpostpass-ilp | David Monniaux | 2019-03-12 | 1 | -2/+4 |
| | | |||||
* | | better tracing for ILP + make clean | David Monniaux | 2019-03-12 | 2 | -3/+7 |
|/ | |||||
* | Fix for frame pointer being destroyed | Cyril SIX | 2019-03-12 | 1 | -5/+10 |
| | |||||
* | volatile stores | David Monniaux | 2019-03-10 | 1 | -43/+40 |
| | |||||
* | volatile load | David Monniaux | 2019-03-10 | 1 | -37/+37 |
| | |||||
* | Added error message for Odivfs in Asmblockgen | Cyril SIX | 2019-03-08 | 1 | -0/+1 |
| | |||||
* | 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 | 5 | -42/+387 |
|\ | |||||
| * | 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 |
| | | |||||
| * | Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2) | Cyril SIX | 2019-03-07 | 1 | -10/+14 |
| | | |||||
| * | HACK for Pcompiw/Pcompil as well | Cyril SIX | 2019-03-07 | 1 | -2/+8 |
| | | |||||
| * | 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 |
|/ | |||||
* | 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 |
| |