aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-2018-92/+148
|\
| * More work on test, regression/packedstruct1.c and regression/varargs2.c don't...Cyril SIX2019-09-204-24/+33
| * Adding SIMU=k1-cluster -- in configureCyril SIX2019-09-201-0/+1
| * __builtin_bswap16, 32 and 64Cyril SIX2019-09-204-39/+38
| * Fixing machine description (error in wchar signedness + trying different valu...Cyril SIX2019-09-191-5/+32
| * Desactivating CompCert tests taking too longCyril SIX2019-09-191-1/+3
| * Adding some function calls in interop testsCyril SIX2019-09-192-7/+15
| * Detailing oracle/vérificateur in the timingsCyril SIX2019-09-182-2/+3
| * Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-184-7/+10
| * Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
| * Adding back "exit 2" to the test target of test/c/MakefileCyril SIX2019-09-131-2/+2
| * Scaling down compression testsCyril SIX2019-09-131-5/+11
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-1335-128/+142
|\|
| * Reducing further the input size of the testsCyril SIX2019-09-1330-71/+68
| * Scaling down most of c/ CompCert testsCyril SIX2019-09-1318-37/+56
| * Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-09-1025-107/+559
| |\
| | * Starting to modify official CompCert tests to be passable with the simuCyril SIX2019-09-1018-89/+81
| | * Test for compd.geuCyril SIX2019-09-051-0/+6
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-09-103-6/+6
| |\ \
* | \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-tra...David Monniaux2019-09-104-32/+35
|\ \ \ \ | | |/ / | |/| |
| * | | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-052-5/+5
| * | | Update man page.Bernhard Schommer2019-09-021-1/+1
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-107-18/+472
|\ \ \ \ | | |_|/ | |/| |
| * | | Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-053-18/+1
| * | | Adding tests for cmovedCyril SIX2019-09-052-0/+85
| * | | (#157) Fixing warning for desactivated afaddd builtin. No implementation yetCyril SIX2019-09-051-0/+6
| * | | a dedicated entry-point to the doc of Coq sourcesSylvain Boulmé2019-09-031-0/+380
| | |/ | |/|
* | | missing fileDavid Monniaux2019-09-091-0/+26
* | | -fall-loads-nontrapDavid Monniaux2019-09-095-2/+20
* | | proof for AllnontrapDavid Monniaux2019-09-091-0/+215
* | | finished the proofs for non-trapping loadsDavid Monniaux2019-09-081-10/+21
* | | asmblockgen worksDavid Monniaux2019-09-082-5/+48
* | | more proofs on notrap2David Monniaux2019-09-081-9/+53
* | | more proofs on notrapDavid Monniaux2019-09-081-6/+124
* | | notrap in mppa_k1c ML codeDavid Monniaux2019-09-083-31/+35
* | | a couple "Admitted" and the Coq compilesDavid Monniaux2019-09-081-12/+18
* | | moving forward with notrapDavid Monniaux2019-09-081-22/+10
* | | furtherDavid Monniaux2019-09-081-3/+20
* | | moving forward on K1CDavid Monniaux2019-09-078-171/+200
* | | fix for Risc-VDavid Monniaux2019-09-074-8/+34
* | | PowerPC compilesDavid Monniaux2019-09-076-22/+104
* | | fixes for compiling on other platformsDavid Monniaux2019-09-074-8/+8
* | | fixes for ARMDavid Monniaux2019-09-079-42/+86
* | | notrap works on x86David Monniaux2019-09-071-12/+3
* | | more for passing notrap through x86David Monniaux2019-09-076-12/+66
* | | for nontrapDavid Monniaux2019-09-061-0/+28
* | | ONE "admitted" and things compileDavid Monniaux2019-09-0612-46/+87
* | | progress in proofDavid Monniaux2019-09-051-14/+27
* | | BSload notrap1David Monniaux2019-09-051-1/+19
* | | moving forward with proofsDavid Monniaux2019-09-052-29/+29
generated by cgit (git 2.34.1) at 2024-07-12 03:51:32 +0000