aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-17/+111
* selectl with conditionDavid Monniaux2019-04-051-9/+56
* Select cmpluDavid Monniaux2019-04-051-0/+18
* select cmpuDavid Monniaux2019-04-051-3/+23
* factor out some proofsDavid Monniaux2019-04-051-6/+3
* some more Oselect comparisonsDavid Monniaux2019-04-041-1/+12
* OselectDavid Monniaux2019-04-041-4/+5
* prepare for conditions in cmoveDavid Monniaux2019-04-041-4/+4
* ternary ops for float/doubleDavid Monniaux2019-04-031-0/+28
* ternary ops in AES and TEADavid Monniaux2019-04-031-2/+2
* Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-031-74/+232
|\
| * Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-29/+157
| * Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-031-25/+84
| * We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-031-34/+6
| * Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-13/+12
* | selectl generationDavid Monniaux2019-03-261-3/+13
* | selectlDavid Monniaux2019-03-251-0/+14
* | more on cmoveDavid Monniaux2019-03-251-63/+24
|/
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-3/+3
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-081-2/+310
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| * Fix minor proofCyril SIX2019-03-071-0/+91
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-31/+23
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-10/+16
|/
* Added double comparisonsCyril SIX2019-03-011-0/+70
* Ajouté la négation des comparateurs singleCyril SIX2019-03-011-1/+39
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+32
* OshrxlimmCyril SIX2019-02-081-16/+17
* Removing the low_half axiomCyril SIX2019-02-051-16/+18
* Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ...Cyril SIX2019-01-291-33/+45
* Added sxwd and zxwd supportCyril SIX2019-01-221-5/+5
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-98/+98
* MBload provedCyril SIX2018-11-071-18/+12
* MBop provedCyril SIX2018-11-071-95/+97
* Changes in Asmblockgenproof1 -> MBcond provedCyril SIX2018-11-071-28/+45
* MBcond false proven (modulo change needed in Asmblockgenproof1)Cyril SIX2018-11-071-5/+5
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-061-24/+35
* Début de MBcondCyril SIX2018-11-051-60/+64
* MBtailcall proofCyril SIX2018-10-291-12/+8
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-261-15/+17
* MBgetparam done!Cyril SIX2018-10-241-5/+3
* MBsetstack done!Cyril SIX2018-10-241-26/+17
* Avancement dans le cas MBgetstack du step_simu_basicCyril SIX2018-10-181-5/+6
* Preuve du internal_function (step_simulation)Cyril SIX2018-09-281-6/+7
* storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-271-15/+29
* Enlèvement du "no_builtin" condition; exec_control sur les option control; e...Cyril SIX2018-09-261-10/+17
* AB: removing bregsCyril SIX2018-09-261-3/+3
* MB2AB - Adding Asmblockgenproof1.vCyril SIX2018-09-261-0/+1595
generated by cgit (git 2.34.1) at 2024-07-06 18:02:47 +0000