aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added back bitslices-aesCyril SIX2019-05-154-32/+17
|
* Avancement sur la génération de Makefile des benchmarksCyril SIX2019-05-1434-409/+84
|
* some lemmas on division etc.David Monniaux2019-05-141-0/+258
|
* sum with moduloDavid Monniaux2019-05-131-0/+18
|
* 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-135-27/+60
|
* we directly call 64-bit unsigned divisionDavid Monniaux2019-05-134-26/+24
|
* begin proving that we can use 64-bit division for doing 32David Monniaux2019-05-131-0/+64
|
* clock the time in heptagonDavid Monniaux2019-05-131-0/+8
|
* new example + moved random number generator to common filesDavid Monniaux2019-05-1316-24/+1185
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-05-131-3/+16
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge branch 'mppa-work' of ↵David Monniaux2019-05-123-64/+72
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | directly branch to certain division functions from gccDavid Monniaux2019-05-121-3/+16
| | |
* | | Merge branch 'mppa-work' of ↵David Monniaux2019-05-103-64/+72
|\ \ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Asmblockgen prologue is now 1 basicblock (instead of 3)Cyril SIX2019-05-103-64/+72
| |/
* | Merge branch 'mppa-work' of ↵David Monniaux2019-05-1017-81/+5267
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge branch 'mppa-work' of ↵David Monniaux2019-05-093-56/+165
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| | * Exploiting immediate comparisonsCyril SIX2019-05-092-36/+145
| | |
| | * Replacing tabs by spaces in TargetPrinterCyril SIX2019-05-091-20/+20
| | |
| * | DM manual inliningDavid Monniaux2019-05-091-22/+25
| |/
| * smart memcpy for arbitrary sizesDavid Monniaux2019-05-092-12/+30
| |
| * with -en (expand main node)David Monniaux2019-05-096-0/+3569
| |
| * copy 16 by 16David Monniaux2019-05-092-14/+15
| |
| * slightly improved memcpyDavid Monniaux2019-05-091-12/+23
| |
| * structure copy through 4 byte registers instead of 1David Monniaux2019-05-091-24/+47
| |
| * Lustre "convertible" compilé avec -2cgcDavid Monniaux2019-05-096-0/+1452
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-05-0922-81/+2251
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * carlightV2 example from Lustre V6David Monniaux2019-05-084-89/+111
| |
| * carlightDavid Monniaux2019-05-083-0/+467
| |
| * added clockDavid Monniaux2019-05-081-1/+9
| |
| * removed print statementsDavid Monniaux2019-05-081-81/+18
| |
| * from Lustre v6 examplesDavid Monniaux2019-05-086-0/+1745
| |
| * simplification d'un code moche pour les variables thread-localDavid Monniaux2019-05-081-1/+1
| |
| * generalize bblock_equiv into bblock_simu (abstract_bb)Sylvain Boulmé2019-05-076-73/+59
| |
| * fix linking bug (my fault)David Monniaux2019-05-071-1/+1
| |
| * put the get ra in same bundle as allocframeDavid Monniaux2019-05-071-1/+1
| |
| * gain d'un cycle au moment du freeframe (passer au ret dans le même bundle)David Monniaux2019-05-071-1/+6
| |
| * Merge branch 'mppa-work' of ↵David Monniaux2019-05-074-29/+28
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * \ Merge branch 'mppa-work' of ↵David Monniaux2019-05-064-267/+74
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | | one cycle less in allocframeDavid Monniaux2019-05-061-3/+3
| | | |
| * | | wrong srsd arith unit assignmentDavid Monniaux2019-05-051-2/+2
| | | |
* | | | Merge branch 'mppa-work' of ↵David Monniaux2019-05-074-29/+28
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | | generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-074-29/+28
| | |/ | |/|
* | | Merge branch 'mppa-work' of ↵David Monniaux2019-05-064-267/+74
|\| | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workCyril SIX2019-05-064-267/+74
| |\ \ | | |/ | |/|
| | * simplification semantique+preuve des load_q+load_oSylvain Boulmé2019-05-064-267/+74
| | |
* | | oubli DecBoolOps.vDavid Monniaux2019-05-061-1/+1
|/ /
* | little fixDavid Monniaux2019-05-041-1/+1
| |
* | load code into I-cacheDavid Monniaux2019-05-041-0/+3
| |
* | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-0411-27/+465
|\|
| * generates loDavid Monniaux2019-05-041-1/+21
| |
generated by cgit (git 2.34.1) at 2024-07-11 22:52:31 +0000