aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
Commit message (Expand)AuthorAgeFilesLines
* 32-bit rotate finishedDavid Monniaux2019-03-161-1/+2
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-2/+2
* Refactorisation des load et des storeCyril SIX2019-03-081-32/+32
* Refactorized Asmblock exec_basic_instrCyril SIX2019-03-081-104/+120
* axioms on pointer comparison removed !Sylvain Boulmé2019-03-071-11/+12
* remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-18/+46
* Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-9/+30
* Added double comparisonsCyril SIX2019-03-011-1/+14
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+49
* Ointuofsingle doneCyril SIX2019-03-011-0/+2
* Float conversion fixes + some more conversionsCyril SIX2019-02-271-2/+14
* Proving the trans_block_header axiomsCyril SIX2019-02-271-0/+30
* Remove unnecessary and error prone FR constructor for pregsCyril SIX2019-02-201-5/+2
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-151-6/+33
* Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-121-0/+4
* Added Ointofsingle + floatconv unit testCyril SIX2019-02-121-1/+3
* Added OsingleofintCyril SIX2019-02-121-0/+2
* Added Ofloatconst and Osingleconst (not integrated in scheduler yet)Cyril SIX2019-02-121-0/+23
* Added indirect tailcallsCyril SIX2019-02-081-0/+3
* Removing the low_half axiomCyril SIX2019-02-051-25/+21
* Adding indirect calls (icall instruction)Cyril SIX2019-01-291-0/+3
* Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ...Cyril SIX2019-01-291-2/+2
* Adding a predicate that a builtin must be alone in its basicblockCyril SIX2019-01-231-79/+139
* Added sxwd and zxwd supportCyril SIX2019-01-221-4/+4
* Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-051-4/+8
* Moving size_blocks from Asmblockgen to AsmblockCyril SIX2018-12-051-0/+8
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-12/+13
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-1/+11
* Déterminisme prouvé -> Tout est prouvéCyril SIX2018-11-081-1/+59
* Proved non_empty_bblock_refl (was Admitted)Cyril SIX2018-11-081-4/+4
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-261-0/+35
* Adding "proof irrelevance" to bblocksCyril SIX2018-10-251-15/+49
* MBsetstack done!Cyril SIX2018-10-241-2/+2
* step_simulation_bblock is back!Cyril SIX2018-10-241-1/+1
* ajoute un axiom a virer plus tardSylvain Boulmé2018-10-231-1/+7
* Un peu d'avancement dans exec_straight_control et cieCyril SIX2018-10-081-13/+12
* Fini le cas du step_simu_control où il n'y a pas de exitCyril SIX2018-10-041-14/+9
* Schéma de simulation + les Pnop sont maintenant implicitesCyril SIX2018-10-031-8/+22
* Removed the bundle attemptCyril SIX2018-09-281-47/+7
* Enlèvement du "no_builtin" condition; exec_control sur les option control; e...Cyril SIX2018-09-261-12/+25
* AB: removing bregsCyril SIX2018-09-261-68/+37
* MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-8/+6
* MB2AB - Proof of external function stepCyril SIX2018-09-251-7/+7
* relectureSylvain Boulmé2018-09-241-1/+3
* a few stubs for bundlingSylvain Boulmé2018-09-241-194/+0
* one step toward "bundle_step"Sylvain Boulmé2018-09-241-6/+55
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-249/+259
* Asmblockgen: Added Pnop and Program DefinitionsCyril SIX2018-09-061-38/+7
* Example of Program use...Sylvain Boulmé2018-09-061-0/+16
* Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-061-0/+2
generated by cgit (git 2.34.1) at 2024-07-06 17:29:51 +0000