aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgen.v
Commit message (Expand)AuthorAgeFilesLines
* 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:30:44 +0000