aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* disable useless warningsDavid Monniaux2019-03-084-4/+4
|
* Rajout de commentaires sur les instructions non émisesCyril SIX2019-03-081-8/+8
|
* Fix for the compw immediate problemCyril SIX2019-03-081-7/+17
|
* Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)Cyril SIX2019-03-081-8/+8
|
* Refactorisation des load et des storeCyril SIX2019-03-083-62/+40
|
* Reverting the hack introduces on Pcompw etc..Cyril SIX2019-03-081-14/+3
|
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-089-45/+394
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| |
| * Fix minor proofCyril SIX2019-03-073-27/+142
| |
| * stop warning about system includesDavid Monniaux2019-03-073-3/+3
| |
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
| |
| * Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-071-2/+8
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| | * HACK for Pcompiw/Pcompil as wellCyril SIX2019-03-071-2/+8
| | |
| * | forgot the .hDavid Monniaux2019-03-071-0/+4
| |/
| * HACK for the Pcompw/Pcompl memory problem (but performance decrease, to ↵Cyril SIX2019-03-061-1/+4
| | | | | | | | remove later)
* | Fixing Asmblockdeps proofsCyril SIX2019-03-081-147/+21
| |
* | Refactorized Asmblock exec_basic_instrCyril SIX2019-03-082-105/+121
| |
* | axioms on pointer comparison removed !Sylvain Boulmé2019-03-071-11/+12
| |
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-073-66/+77
| | | | | | | | | | | | TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-073-21/+48
|/
* Merge branch 'mppa_postpass' of ↵Sylvain Boulmé2019-03-063-3/+63
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-052-20/+218
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-056-81/+24
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-057-85/+187
| |\ \ \ | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-0224-1377/+2286
| |\ \ \ \ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-221-5/+131
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ \ \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-212-26/+101
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ \ \ \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-201-31/+41
| |\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * \ \ \ \ \ \ \ Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-2012-98/+701
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * | | | | | | | | mul8: loop-invariant code motionDavid Monniaux2019-02-193-3/+63
| | | | | | | | | |
* | | | | | | | | | fix eq sur OIncremPCSylvain Boulmé2019-03-061-7/+14
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
* | | | | | | | | quick fix of equalities issuesSylvain Boulmé2019-03-052-1/+10
| | | | | | | | |
* | | | | | | | | Added pretty printersCyril SIX2019-03-051-19/+208
| |_|_|_|_|_|_|/ |/| | | | | | |
* | | | | | | | fix extraction of ImpConfigSylvain Boulmé2019-03-051-2/+5
| | | | | | | |
* | | | | | | | compilation of ImpIOOraclesSylvain Boulmé2019-03-053-5/+9
| | | | | | | |
* | | | | | | | No more axioms remaining (scheduling completely proven), however error at ↵Cyril SIX2019-03-052-74/+10
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | extraction
* | | | | | | C'est moi qui avait fait des betises avec CoqIDE, ça remarcheCyril SIX2019-03-051-8/+26
| | | | | | |
* | | | | | | [BROKEN] error with the new is_constant and is_constant_correctCyril SIX2019-03-051-26/+8
| | | | | | |
* | | | | | | forward_simu_alt proof AsmblockdepsCyril SIX2019-03-051-1/+6
| | | | | | |
* | | | | | | remove cumbersome dependency on genv in bblock_eq_testSylvain Boulmé2019-03-054-33/+55
| | | | | | |
* | | | | | | No more axiom remaining in PostpassScheduling.v (but still a couple ↵Cyril SIX2019-03-053-46/+66
| | | | | | | | | | | | | | | | | | | | | | | | | | | | remaining in Asmblockdeps)
* | | | | | | bblock_equiv_reduce Asmblockdeps.vCyril SIX2019-03-041-4/+42
| | | | | | |
* | | | | | | (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-022-2/+19
| |_|_|_|_|/ |/| | | | |
* | | | | | Added double comparisonsCyril SIX2019-03-018-23/+118
| | | | | |
* | | | | | Ajouté la négation des comparateurs singleCyril SIX2019-03-013-3/+42
| | | | | |
* | | | | | Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-018-29/+132
| | | | | |
* | | | | | Ointuofsingle doneCyril SIX2019-03-016-32/+23
| | | | | |
* | | | | | Added long double = double by default on Kalray architectureCyril SIX2019-03-011-1/+1
| | | | | |
* | | | | | Float conversion fixes + some more conversionsCyril SIX2019-02-2715-34/+123
| | | | | |
* | | | | | Fixed some additional operands inversionsCyril SIX2019-02-271-4/+4
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-11 22:46:15 +0000