aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* -fpostpass-ilpDavid Monniaux2019-03-125-16/+3
* script for using Gurobi with -fpostpass-ilpDavid Monniaux2019-03-121-0/+3
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-125-110/+141
|\
| * Added cascaded_scheduler but the flag does not workCyril SIX2019-03-122-3/+4
| * Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-125-3/+12
| * 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-123-2/+7
* | better tracing for ILP + make cleanDavid Monniaux2019-03-123-3/+12
* | Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-121-5/+10
|\|
| * Fix for frame pointer being destroyedCyril SIX2019-03-121-5/+10
* | forgot a free()David Monniaux2019-03-121-0/+1
* | simpler MakefilesDavid Monniaux2019-03-121-0/+12
|/
* et hop un Makefile pour les matrices complexesDavid Monniaux2019-03-122-0/+12
* some more optimized complex matrixDavid Monniaux2019-03-121-12/+9
* easier for clocking directly from ccomp filesDavid Monniaux2019-03-122-0/+5
* some more work on complex matricesDavid Monniaux2019-03-121-8/+195
* some more about complex numbersDavid Monniaux2019-03-111-8/+49
* wrong directory, fixedDavid Monniaux2019-03-111-0/+0
* et hop un MakefileDavid Monniaux2019-03-111-0/+9
* complex numbers attemptDavid Monniaux2019-03-101-0/+22
* test code for jump tablesDavid Monniaux2019-03-101-0/+34
* varargsDavid Monniaux2019-03-102-18/+2
* forgot the MakefileDavid Monniaux2019-03-101-0/+18
* test for volatilesDavid Monniaux2019-03-101-0/+33
* volatile storesDavid Monniaux2019-03-103-45/+42
* volatile loadDavid Monniaux2019-03-101-37/+37
* demo for volatileDavid Monniaux2019-03-092-9/+28
* program for testing volatilesDavid Monniaux2019-03-091-0/+32
* store the assembly source code as wellDavid Monniaux2019-03-091-5/+8
* code qui planteDavid Monniaux2019-03-083-0/+33
* Modified test/c/Makefile for CompCert tests (remove all the float tests with ...Cyril SIX2019-03-082-5/+6
* Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-081-0/+1
|\
| * Added error message for Odivfs in AsmblockgenCyril SIX2019-03-081-0/+1
* | un example avec varargs flottantsDavid Monniaux2019-03-081-0/+34
|/
* disable useless warningsDavid Monniaux2019-03-084-4/+4
* 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-089-45/+394
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| * Fix minor proofCyril SIX2019-03-073-27/+142
| * stop warning about system includesDavid Monniaux2019-03-073-3/+3
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
| * Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-03-071-2/+8
| |\
generated by cgit (git 2.34.1) at 2024-07-12 00:02:18 +0000