aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/lib
Commit message (Expand)AuthorAgeFilesLines
* Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
* Englishification of commentsCyril SIX2019-09-032-11/+6
* move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-1134/+0
* move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+1368
* Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-workCyril SIX2019-05-202-15/+52
|\
| * extract Machgen.trans_code stuff from AsmgenproofSylvain Boulmé2019-04-071-15/+1
| * squelette de preuve pour Machblockgenproof.vSylvain Boulmé2019-02-221-0/+51
* | generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-071-5/+4
* | simplification semantique+preuve des load_q+load_oSylvain Boulmé2019-05-061-4/+2
* | big proofs for so / loDavid Monniaux2019-05-041-0/+18
* | begin add PlqDavid Monniaux2019-05-031-0/+7
* | rm OfslowDavid Monniaux2019-05-031-1/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-031-2/+2
|\ \
| * | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-2/+2
* | | getting stuck need to move offsetsDavid Monniaux2019-05-031-0/+7
|/ /
* | it compilesDavid Monniaux2019-05-011-0/+1
* | begin load.xsDavid Monniaux2019-05-011-0/+1
* | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-1/+1
|\ \
| * | relecture sylvainSylvain Boulmé2019-04-051-1/+1
* | | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-5/+15
|/ /
* | #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-3/+3
* | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-4/+4
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-8/+10
* | Plugged Asmblockdeps into PostpassSchedulingCyril SIX2019-02-251-1/+7
* | Removing the low_half axiomCyril SIX2019-02-051-4/+4
|/
* Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-262-0/+1421
generated by cgit (git 2.34.1) at 2024-07-06 17:05:27 +0000