aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof0.v
Commit message (Expand)AuthorAgeFilesLines
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-211-0/+18
* Proved MBstore -> all instructions are provedCyril SIX2018-11-081-8/+0
* MBop provedCyril SIX2018-11-071-7/+1
* MBcond true proved (but a small change needs to be done to Asmblockgenproof1)Cyril SIX2018-11-061-0/+15
* Setting ep to false when the basicblock has a header. MBgoto done. MBgetparam...Cyril SIX2018-10-311-0/+97
* MBtailcall proofCyril SIX2018-10-291-12/+18
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-261-17/+19
* MBbuiltin provedCyril SIX2018-10-261-0/+68
* Commencé à réintroduire du "ep" qui a du sensCyril SIX2018-10-191-16/+17
* Avancement du schéma. A voir problème des tracesCyril SIX2018-10-101-3/+15
* Un peu d'avancement dans exec_straight_control et cieCyril SIX2018-10-081-12/+69
* Removed the bundle attemptCyril SIX2018-09-281-2/+2
* Preuve du internal_function (step_simulation)Cyril SIX2018-09-281-7/+48
* storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-271-3/+1
* 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-261-31/+76
* AB: removing bregsCyril SIX2018-09-261-6/+8
* MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-2/+132
* MB2AB - Proof of external function stepCyril SIX2018-09-251-2/+57
* MB2AB - Trois premières parties du lock-stepCyril SIX2018-09-211-1/+301
* return_address_exists -> doneSylvain Boulmé2018-09-201-3/+1
* avancement return_addressSylvain Boulmé2018-09-201-45/+64
* return_address suiteSylvain Boulmé2018-09-191-3/+111
* proof sketch for Asmgenproof.return_address_exists ?Sylvain Boulmé2018-09-191-0/+4
* premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-181-0/+95
generated by cgit (git 2.34.1) at 2024-07-06 18:09:03 +0000