aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* now compiles with pthread.hDavid Monniaux2019-04-101-4/+1
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-04-105-14/+12
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Fixing missing features in Asmexpand.ml (EF_annot, EF_annot_val, EF_inline_asm)Cyril SIX2019-04-091-9/+6
| |
| * Disabling the packedstruct tests from test/regressionCyril SIX2019-04-091-1/+2
| |
| * All CompCert tests can be compiledCyril SIX2019-04-093-4/+4
| |
* | for killing _PragmaDavid Monniaux2019-04-081-0/+1
|/
* exemples d'accès mémoire lentsDavid Monniaux2019-04-083-0/+31
|
* moving iandb from ImpCore to ImpPreludeSylvain Boulmé2019-04-082-23/+18
|
* better explanationDavid Monniaux2019-04-081-4/+26
|
* better intermediate pointDavid Monniaux2019-04-081-5/+8
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-04-081-17/+29
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * improving comments on AsmvliwSylvain Boulmé2019-04-081-17/+29
| |
* | powerwindow from tacle-benchDavid Monniaux2019-04-0842-0/+5165
|/
* Merge branch 'mppa-refactor' into mppa-workCyril SIX2019-04-0812-1946/+1667
|\
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-0880-125/+82525
| |\ | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
| * \ Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-088-465/+331
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v
| | * | relecture sylvainSylvain Boulmé2019-04-058-505/+353
| | | | | | | | | | | | | | | | avec TODOs pour refactoring #90
| * | | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-056-257/+89
| |/ /
| * | #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-0511-1611/+1634
| | |
* | | from Tacle BenchDavid Monniaux2019-04-088-0/+618
| |/ |/|
* | predicated experimentsDavid Monniaux2019-04-072-0/+29
| |
* | uses the pattern matchingDavid Monniaux2019-04-061-2/+2
| |
* | keep the .s filesDavid Monniaux2019-04-061-9/+11
| |
* | Makefile for timing.David Monniaux2019-04-062-3/+13
| | | | | | | | We are 12% slower than gcc.
* | makefile for PCRE2David Monniaux2019-04-063-5/+12764
| |
* | tests with PCRE2 (regular expression library)David Monniaux2019-04-0639-0/+62943
| |
* | use ternary in fillDavid Monniaux2019-04-061-1/+1
| |
* | reoptimize the CDavid Monniaux2019-04-061-1/+2
| |
* | hand optimizationsDavid Monniaux2019-04-061-2/+4
| |
* | various hand optimizationsDavid Monniaux2019-04-065-0/+1525
| |
* | reoptimize by handDavid Monniaux2019-04-061-3/+2
| |
* | goto endDavid Monniaux2019-04-061-2/+25
| |
* | there seems to be some cache preload involved?David Monniaux2019-04-061-1/+2
| |
* | use of ternary operatorsDavid Monniaux2019-04-061-3/+28
| |
* | hand optimizationsDavid Monniaux2019-04-062-0/+407
| |
* | have one with specific positionDavid Monniaux2019-04-061-1/+1
| |
* | no need for this to be in two_address_opDavid Monniaux2019-04-062-2/+2
| |
* | binary search from Rosetta CodeDavid Monniaux2019-04-062-0/+78
| |
* | ternary op version of bitsliced TEADavid Monniaux2019-04-051-4/+9
| |
* | use cmove in bitsliced AESDavid Monniaux2019-04-051-5/+2
| |
* | move patterns to include fileDavid Monniaux2019-04-052-14/+25
| |
* | implement using our "pattern matching"David Monniaux2019-04-051-4/+11
| |
* | reinstated the orl selectl constructDavid Monniaux2019-04-052-10/+7
| |
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
| |
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
| |
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-054-74/+8
| |
* | Oselectf, Oselectfs with conditionDavid Monniaux2019-04-058-131/+325
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-051-1/+1
|\|
| * Possible fix pour l'issue #82 (mauvais calcul de taille de bundle pour les ↵Cyril SIX2019-04-051-1/+1
| | | | | | | | store)
* | selectl with conditionDavid Monniaux2019-04-058-68/+172
| |
generated by cgit (git 2.34.1) at 2024-07-11 22:50:36 +0000