aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* dealing with permutationsSylvain Boulmé2019-03-272-29/+100
* Avancement dans Asmblockdeps.vCyril SIX2019-03-272-91/+113
* 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
* Un peu d'avancementCyril SIX2019-03-262-4/+287
* slight simplificationSylvain Boulmé2019-03-231-5/+4
* Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
* fix for Coq.8.8 ??Sylvain Boulmé2019-03-222-4/+3
* Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu...Cyril SIX2019-03-222-1/+72
* simplification of the proofSylvain Boulmé2019-03-212-29/+70
* yet another step backwardSylvain Boulmé2019-03-201-18/+39
* one step further...Sylvain Boulmé2019-03-201-6/+28
* premier decoupageSylvain Boulmé2019-03-201-2/+56
* Integrating Asmvliw.v in the proof chainCyril SIX2019-03-203-16/+29
* Idée de preuve VLIWCyril SIX2019-03-181-2/+21
* fix the step_internal of AsmvliwSylvain Boulmé2019-03-141-19/+23
* definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
* Corrigé certaines latences (Store -> 1 i/o 3, Set -> 4 i/o 3)Cyril SIX2019-03-131-4/+3
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-133-25/+25
* for using CPlexDavid Monniaux2019-03-131-1/+12
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-122-109/+134
|\
| * Added cascaded_scheduler but the flag does not workCyril SIX2019-03-121-1/+1
| * Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-121-2/+3
| * Proof of exec_trans_pcincr solvedCyril SIX2019-03-121-7/+31
| * Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheckCyril SIX2019-03-121-12/+12
| |\
| | * fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)Sylvain Boulmé2019-03-121-12/+12
| * | Simplification des preuves "de discrimination" dans AsmblockdepsCyril SIX2019-03-121-94/+77
| |/
| * [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-122-1/+19
* | -fpostpass-ilpDavid Monniaux2019-03-121-2/+4
* | better tracing for ILP + make cleanDavid Monniaux2019-03-122-3/+7
|/
* Fix for frame pointer being destroyedCyril SIX2019-03-121-5/+10
* volatile storesDavid Monniaux2019-03-101-43/+40
* volatile loadDavid Monniaux2019-03-101-37/+37
* Added error message for Odivfs in AsmblockgenCyril SIX2019-03-081-0/+1
* Rajout de commentaires sur les instructions non émisesCyril SIX2019-03-081-8/+8
* Fix for the compw immediate problemCyril SIX2019-03-081-7/+17
* Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)Cyril SIX2019-03-081-8/+8
* Refactorisation des load et des storeCyril SIX2019-03-083-62/+40
* Reverting the hack introduces on Pcompw etc..Cyril SIX2019-03-081-14/+3
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-085-42/+387
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| * Fix minor proofCyril SIX2019-03-073-27/+142
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
| * HACK for Pcompiw/Pcompil as wellCyril SIX2019-03-071-2/+8
| * HACK for the Pcompw/Pcompl memory problem (but performance decrease, to remov...Cyril SIX2019-03-061-1/+4
* | Fixing Asmblockdeps proofsCyril SIX2019-03-081-147/+21
* | Refactorized Asmblock exec_basic_instrCyril SIX2019-03-082-105/+121
* | axioms on pointer comparison removed !Sylvain Boulmé2019-03-071-11/+12
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-073-66/+77
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-073-21/+48
|/
generated by cgit (git 2.34.1) at 2024-07-14 07:28:49 +0000