aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Added indirect tailcallsCyril SIX2019-02-081-1/+24
|
* Adding indirect calls (icall instruction)Cyril SIX2019-01-291-1/+21
|
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-18/+18
|
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-0/+1
|
* Proved MBstore -> all instructions are provedCyril SIX2018-11-081-4/+25
|
* MBload provedCyril SIX2018-11-071-1/+25
|
* MBop provedCyril SIX2018-11-071-2/+30
|
* MBcond false proven (modulo change needed in Asmblockgenproof1)Cyril SIX2018-11-071-1/+27
|
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-061-6/+69
|
* Début de MBcondCyril SIX2018-11-051-0/+15
|
* MBreturn doneCyril SIX2018-11-051-5/+22
|
* Got the schema working again with the headersCyril SIX2018-11-051-30/+57
|
* Trying to change the proofs for the new ep. Stuck in step_simu_bblock'Cyril SIX2018-10-311-39/+68
|
* Setting ep to false when the basicblock has a header. MBgoto done. ↵Cyril SIX2018-10-311-45/+192
| | | | MBgetparam needs fix
* MBtailcall proofCyril SIX2018-10-291-8/+28
|
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-261-25/+80
|
* MBbuiltin provedCyril SIX2018-10-261-427/+121
|
* Enlèvement de Pnop inutiles pour le PbuiltinCyril SIX2018-10-261-11/+30
|
* MBgetparam done!Cyril SIX2018-10-241-3/+58
|
* MBsetstack done!Cyril SIX2018-10-241-5/+19
|
* MBgetstack proof done!Cyril SIX2018-10-241-18/+9
|
* step_simulation_bblock is back!Cyril SIX2018-10-241-171/+76
|
* ajoute un axiom a virer plus tardSylvain Boulmé2018-10-231-4/+10
|
* Avancement dans le schéma. Blocage sur step_simu_bblock'Cyril SIX2018-10-231-72/+219
|
* New definition of Codestate, new matchCyril SIX2018-10-221-98/+105
|
* Commencé à réintroduire du "ep" qui a du sensCyril SIX2018-10-191-53/+88
|
* Avancement dans le cas MBgetstack du step_simu_basicCyril SIX2018-10-181-6/+58
|
* Squelette du step_simu_basicCyril SIX2018-10-161-20/+66
|
* step_simu_control with MBcall and exit=None are back onlineCyril SIX2018-10-161-44/+9
|
* step_simulation_bblock' is back online, using exec_body instead of exec_straightCyril SIX2018-10-161-19/+74
|
* transl_blocks de nouveau prouvé + Ltac exploreInstCyril SIX2018-10-161-20/+73
|
* Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du ↵Cyril SIX2018-10-151-68/+71
| | | | transl_bblocks_distrib
* Disjonction des cas MB.body bb = nil ou nonCyril SIX2018-10-121-5/+7
|
* Stuck on proving step_simu_bodyCyril SIX2018-10-121-1588/+1622
|
* Separating the case of MBbuiltin from the restCyril SIX2018-10-121-16/+24
|
* Avancement du schéma. A voir problème des tracesCyril SIX2018-10-101-243/+71
|
* Preuve de MBcall et du exit=None dans le step_simu_controlCyril SIX2018-10-101-31/+113
|
* Beaucoup de quincaillerie avec les transl_blocks, travail en coursCyril SIX2018-10-091-23/+116
|
* Un peu d'avancement dans exec_straight_control et cieCyril SIX2018-10-081-32/+105
|
* Fini le cas du step_simu_control où il n'y a pas de exitCyril SIX2018-10-041-20/+50
|
* Schéma de simulation + les Pnop sont maintenant implicitesCyril SIX2018-10-031-15/+88
|
* match_codestate et match_asmblockCyril SIX2018-10-021-33/+142
|
* Separation de step_simulation_bblock en step_simu_control et step_simu_basicCyril SIX2018-10-011-5/+62
|
* Preuve du internal_function (step_simulation)Cyril SIX2018-09-281-23/+35
|
* storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-271-4/+3
|
* Enlèvement du "no_builtin" condition; exec_control sur les option control; ↵Cyril SIX2018-09-261-2/+2
| | | | exec_straight_blocks
* AB: removing bregsCyril SIX2018-09-261-1/+1
|
* MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-4/+76
|
* MB2AB - Proof of external function stepCyril SIX2018-09-251-4/+21
|
* relectureSylvain Boulmé2018-09-241-12/+1
|
generated by cgit (git 2.34.1) at 2024-07-12 09:14:21 +0000