aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-101-1/+1
* Moved some theoremsCyril SIX2020-02-101-13/+0
* Converting Asm.v and Asmblockgenproof.v back to Unix formatCyril SIX2019-12-031-1673/+1673
* finish mergeDavid Monniaux2019-12-021-10/+19
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-173/+128
|\
| * Few minor other changes in proofCyril SIX2019-10-151-3/+3
| * More elaborate comments + rewriting for easier to understand Asmblockgenproof.vCyril SIX2019-10-151-145/+89
| * Fixing fp_is_parent too weak (#165)Cyril SIX2019-10-111-1797/+1808
| * Asmblockgenproof : cur rewritingCyril SIX2019-10-011-11/+11
| * Asmblockgenproof renaming fpok --> epCyril SIX2019-10-011-11/+11
* | asmblockgen worksDavid Monniaux2019-09-081-4/+47
* | moving forward with notrapDavid Monniaux2019-09-081-22/+10
* | furtherDavid Monniaux2019-09-081-3/+20
* | more stuff on non trapping loadsDavid Monniaux2019-09-051-0/+8
|/
* Asmblockgen prologue is now 1 basicblock (instead of 3)Cyril SIX2019-05-101-35/+45
* it compilesDavid Monniaux2019-05-011-1/+1
* translate load.xsDavid Monniaux2019-05-011-1/+1
* make_prologue à partDavid Monniaux2019-04-241-3/+3
* Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-10/+10
|\
| * relecture sylvainSylvain Boulmé2019-04-051-10/+10
* | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-2/+2
|/
* #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-051-14/+14
* Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-3/+3
* We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-031-451/+5
* Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
* Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
* on avance sur la jumptableDavid Monniaux2019-03-221-3/+2
* jumptable avanceDavid Monniaux2019-03-221-1/+8
* Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-1/+2
* The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-2/+2
* Fix minor proofCyril SIX2019-03-071-2/+14
* Added double comparisonsCyril SIX2019-03-011-0/+2
* Ajouté la négation des comparateurs singleCyril SIX2019-03-011-0/+1
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+1
* Remove unnecessary and error prone FR constructor for pregsCyril SIX2019-02-201-3/+3
* Added indirect tailcallsCyril SIX2019-02-081-1/+24
* Adding indirect calls (icall instruction)Cyril SIX2019-01-291-1/+21
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-18/+18
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-0/+1
* Proved MBstore -> all instructions are provedCyril SIX2018-11-081-4/+25
* MBload provedCyril SIX2018-11-071-1/+25
* MBop provedCyril SIX2018-11-071-2/+30
* MBcond false proven (modulo change needed in Asmblockgenproof1)Cyril SIX2018-11-071-1/+27
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-061-6/+69
* Début de MBcondCyril SIX2018-11-051-0/+15
* MBreturn doneCyril SIX2018-11-051-5/+22
* Got the schema working again with the headersCyril SIX2018-11-051-30/+57
* Trying to change the proofs for the new ep. Stuck in step_simu_bblock'Cyril SIX2018-10-311-39/+68
* Setting ep to false when the basicblock has a header. MBgoto done. MBgetparam...Cyril SIX2018-10-311-45/+192
* MBtailcall proofCyril SIX2018-10-291-8/+28
generated by cgit (git 2.34.1) at 2024-07-12 00:19:32 +0000