aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgen.v
Commit message (Expand)AuthorAgeFilesLines
* 32-bit rotate finishedDavid Monniaux2019-03-161-1/+4
* Added error message for Odivfs in AsmblockgenCyril SIX2019-03-081-0/+1
* Rajout de commentaires sur les instructions non émisesCyril SIX2019-03-081-8/+8
* Fix minor proofCyril SIX2019-03-071-25/+37
* Added double comparisonsCyril SIX2019-03-011-20/+20
* Ajouté la négation des comparateurs singleCyril SIX2019-03-011-2/+2
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-28/+20
* Ointuofsingle doneCyril SIX2019-03-011-29/+11
* Float conversion fixes + some more conversionsCyril SIX2019-02-271-0/+24
* Removing unused cases AsmblockgenCyril SIX2019-02-271-3/+0
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-151-99/+43
* Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-121-0/+6
* Added Ointofsingle + floatconv unit testCyril SIX2019-02-121-1/+4
* Added OsingleofintCyril SIX2019-02-121-13/+12
* Added Ofloatconst and Osingleconst (not integrated in scheduler yet)Cyril SIX2019-02-121-10/+4
* Added indirect tailcallsCyril SIX2019-02-081-2/+2
* OshrxlimmCyril SIX2019-02-081-1/+7
* Rajouté des erreurs plus explicites dans Asmblockgen.vCyril SIX2019-01-301-13/+57
* give meaningful "unhandled instr" messagesDavid Monniaux2019-01-291-11/+7
* Adding indirect calls (icall instruction)Cyril SIX2019-01-291-3/+3
* Adding a predicate that a builtin must be alone in its basicblockCyril SIX2019-01-231-2/+6
* Added sxwd and zxwd supportCyril SIX2019-01-221-9/+4
* Merge branch 'mppa_k1c' into mppa_postpassCyril SIX2019-01-171-13/+13
|\
| * Added an error message for 32-bits division and moduloCyril SIX2018-12-111-13/+13
* | Moving size_blocks from Asmblockgen to AsmblockCyril SIX2018-12-051-9/+0
|/
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-11/+13
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-1/+2
* Modified "Asmgen.*" error messages to "Asmblockgen.*"Cyril SIX2018-11-161-12/+12
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-061-0/+5
* Début de MBcondCyril SIX2018-11-051-2/+2
* MBreturn doneCyril SIX2018-11-051-3/+3
* Setting ep to false when the basicblock has a header. MBgoto done. MBgetparam...Cyril SIX2018-10-311-3/+1
* Enlèvement de Pnop inutiles pour le PbuiltinCyril SIX2018-10-261-5/+8
* Adding "proof irrelevance" to bblocksCyril SIX2018-10-251-5/+6
* Commencé à réintroduire du "ep" qui a du sensCyril SIX2018-10-191-8/+8
* transl_blocks de nouveau prouvé + Ltac exploreInstCyril SIX2018-10-161-9/+31
* Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du transl...Cyril SIX2018-10-151-4/+8
* Stuck on proving step_simu_bodyCyril SIX2018-10-121-3/+8
* Preuve de MBcall et du exit=None dans le step_simu_controlCyril SIX2018-10-101-2/+2
* Un peu d'avancement dans exec_straight_control et cieCyril SIX2018-10-081-2/+2
* Schéma de simulation + les Pnop sont maintenant implicitesCyril SIX2018-10-031-3/+5
* return_address suiteSylvain Boulmé2018-09-191-5/+13
* Rajout d'un return_address_offset. Besoin de changer forward_simu de mach mac...Cyril SIX2018-09-061-2/+2
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-1/+1
* Asmblockgen: Added Pnop and Program DefinitionsCyril SIX2018-09-061-18/+15
* Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-061-19/+19
* Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-061-112/+153
* Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-061-0/+857
generated by cgit (git 2.34.1) at 2024-07-06 17:50:33 +0000