aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
...
* Finished implementation of va_arg + testing doneCyril SIX2018-11-301-4/+8
|
* Wrote some tests on va_arg, need to implement __compcert_va_int32 & cieCyril SIX2018-11-281-5/+4
|
* mppa_k1c compilesCyril SIX2018-11-282-9/+3
|
* compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-282-3/+5
|
* Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-0/+8
|
* Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-263-1585/+322
|
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-237-167/+170
|
* Mise à jour vis à vis de CompCert 3.4Cyril SIX2018-11-216-8/+35
|
* Modified "Asmgen.*" error messages to "Asmblockgen.*"Cyril SIX2018-11-161-12/+12
|
* Merge branch 'mppa_asmbloc_nobreg' into mppa_k1cCyril SIX2018-11-1415-3541/+9460
|\ | | | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmexpand.ml mppa_k1c/TargetPrinter.ml test/mppa/Makefile test/mppa/builtins/clzll.c test/mppa/generate.sh
| * 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. ↵Cyril SIX2018-10-313-48/+290
| | | | | | | | MBgetparam needs fix
| * 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 ↵Cyril SIX2018-10-152-72/+79
| | | | | | | | 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-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
| |
generated by cgit (git 2.34.1) at 2024-07-12 03:16:10 +0000