aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
Commit message (Expand)AuthorAgeFilesLines
* rm Pdiv / PdivuDavid Monniaux2019-03-221-15/+1
* Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-191-0/+45
|\
| * mul immediate beginDavid Monniaux2019-03-191-0/+4
| * maddw dans la générationDavid Monniaux2019-03-181-0/+3
| * ça passe mais pas encore l'oracleDavid Monniaux2019-03-181-0/+38
* | Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-3/+14
* | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...Cyril SIX2019-03-181-0/+16
|\|
| * orn / andn in asmDavid Monniaux2019-03-181-0/+16
* | The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-2/+3
|/
* long nand, nor, nxorDavid Monniaux2019-03-161-0/+12
* nxorDavid Monniaux2019-03-161-0/+4
* partial norwDavid Monniaux2019-03-161-3/+7
* nand is implementedDavid Monniaux2019-03-161-0/+4
* 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
generated by cgit (git 2.34.1) at 2024-07-06 15:15:38 +0000