aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* quick and dirty Makefile fixesSylvain Boulmé2019-01-111-2/+3
* [BROKEN] trying to link the test in mppa_k1c/unittest/postpass_testCyril SIX2019-01-114-35/+43
* [BROKEN] Added infos about sd, infinite loop somewhereCyril SIX2019-01-091-5/+23
* Adding more Asmblock instructions to PostpassSchedulingOracleCyril SIX2019-01-081-14/+108
* Raccordement de InstructionScheduler.ml à PostpassSchedulingOracle.mlCyril SIX2019-01-081-4/+94
* Latency constraints building done in PostpassSchedulingOracle.mlCyril SIX2019-01-081-16/+28
* Reorganized PostpassOracle to separate asmblock instructions from real instru...Cyril SIX2019-01-081-72/+111
* Fixed warnings in InstructionSchedulerCyril SIX2019-01-082-21/+24
* Finished the immediate recognition part, started latency constraintsCyril SIX2019-01-071-19/+78
* [BROKEN] Début d'oracleCyril SIX2018-12-203-1/+1068
* Added a simple postpass oracle that splits a bblock into single instruction b...Cyril SIX2018-12-175-4/+32
* Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-053-41/+98
* Moving size_blocks from Asmblockgen to AsmblockCyril SIX2018-12-052-9/+8
* Renaming PostpassSchedulingProof -> PostpassSchedulingproofCyril SIX2018-12-051-0/+0
* Added definitions and proof sketch for PostpassSchedulingCyril SIX2018-12-042-40/+110
* Tout début de développement d'un postpass Asmblock en CoqCyril SIX2018-12-032-0/+135
* Introducing ;; as Pcomma in Asm.vCyril SIX2018-12-032-65/+67
* 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
|\
| * 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
generated by cgit (git 2.34.1) at 2024-06-03 02:12:22 +0000