aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* 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
* Proved MBstore -> all instructions are provedCyril SIX2018-11-082-12/+25
* MBload provedCyril SIX2018-11-072-19/+37
* MBop provedCyril SIX2018-11-073-104/+128
* Changes in Asmblockgenproof1 -> MBcond provedCyril SIX2018-11-071-28/+45
* MBcond false proven (modulo change needed in Asmblockgenproof1)Cyril SIX2018-11-072-6/+32
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-064-30/+124
* Début de MBcondCyril SIX2018-11-053-62/+81
* MBreturn doneCyril SIX2018-11-052-8/+25
* 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. MBgetparam...Cyril SIX2018-10-313-48/+290
* MBtailcall proofCyril SIX2018-10-293-32/+54
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-264-57/+151
* MBbuiltin provedCyril SIX2018-10-262-427/+189
* Enlèvement de Pnop inutiles pour le PbuiltinCyril SIX2018-10-262-16/+38
* Adding "proof irrelevance" to bblocksCyril SIX2018-10-252-20/+55
* MBgetparam done!Cyril SIX2018-10-242-8/+61
* MBsetstack done!Cyril SIX2018-10-243-33/+38
* MBgetstack proof done!Cyril SIX2018-10-241-18/+9
* step_simulation_bblock is back!Cyril SIX2018-10-242-172/+77
* ajoute un axiom a virer plus tardSylvain Boulmé2018-10-232-5/+17
* 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-194-78/+114
* Avancement dans le cas MBgetstack du step_simu_basicCyril SIX2018-10-182-11/+64
* 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-162-29/+104
* Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du transl...Cyril SIX2018-10-152-72/+79
* Disjonction des cas MB.body bb = nil ou nonCyril SIX2018-10-121-5/+7
* Stuck on proving step_simu_bodyCyril SIX2018-10-122-1591/+1630
* 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-102-246/+86
* Preuve de MBcall et du exit=None dans le step_simu_controlCyril SIX2018-10-102-33/+115
* 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-084-59/+188
* Fini le cas du step_simu_control où il n'y a pas de exitCyril SIX2018-10-042-34/+59
* Schéma de simulation + les Pnop sont maintenant implicitesCyril SIX2018-10-033-26/+115
* 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
* SelectLong.vp fixCyril SIX2018-10-011-8/+4
* Fixed BaR mentions in the ML filesCyril SIX2018-09-282-16/+7
* Removed the bundle attemptCyril SIX2018-09-285-623/+9
* Preuve du internal_function (step_simulation)Cyril SIX2018-09-283-36/+90
* storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-273-22/+33
* Avancement dans exec_straight_throughCyril SIX2018-09-271-9/+51
* Enlèvement du "no_builtin" condition; exec_control sur les option control; e...Cyril SIX2018-09-264-55/+120
generated by cgit (git 2.34.1) at 2024-07-04 02:52:02 +0000