aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof0.v
Commit message (Collapse)AuthorAgeFilesLines
* move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+1134
| | | | This file is specific to our backend.
* Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-1099/+0
|
* 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. ↵Cyril SIX2018-10-311-0/+97
| | | | MBgetparam needs fix
* 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; ↵Cyril SIX2018-09-261-31/+76
| | | | exec_straight_blocks
* 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-11 22:06:44 +0000