aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Adding picosat to the benchesCyril SIX2019-10-022-34/+8
|
* Updating test/monniaux/README.mdCyril SIX2019-10-021-1/+8
|
* (forgot to add glpk to benches.sh)Cyril SIX2019-10-021-1/+1
|
* Intégration de GLPKCyril SIX2019-10-022-37/+7
|
* Asmblockgenproof : cur rewritingCyril SIX2019-10-011-11/+11
|
* Tiny cleanCyril SIX2019-10-011-1/+0
|
* Asmblockgenproof renaming fpok --> epCyril SIX2019-10-011-11/+11
|
* Restored previous input sizes for other backendsCyril SIX2019-09-2553-60/+330
|
* Preferring the (ifeq) approach for removing testsCyril SIX2019-09-251-0/+4
|
* Removing NaNs from TESTS_DIFF (float precision issues..)Cyril SIX2019-09-251-0/+3
|
* varargs2 now work correctly (bis)Cyril SIX2019-09-252-3/+15
|
* Stub for builtins-mppa_k1c.cCyril SIX2019-09-251-0/+72
|
* varargs2 now work correctlyCyril SIX2019-09-251-0/+11
|
* Removing packed structs tests (do not work for now)Cyril SIX2019-09-251-0/+2
|
* (#161) - Fixing vararg bugCyril SIX2019-09-241-2/+2
|
* More work on test, regression/packedstruct1.c and regression/varargs2.c ↵Cyril SIX2019-09-204-24/+33
| | | | don't pass
* 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 ↵Cyril SIX2019-09-191-5/+32
| | | | value for passing structs)
* 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
|
* 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 ↵David Monniaux2019-09-1025-107/+559
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * 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
| |
| * 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
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-09-103-6/+6
|\ \ | |/ |/|
| * Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-052-5/+5
| |
| * Update man page.Bernhard Schommer2019-09-021-1/+1
| | | | | | | | Unused-variables is disabled by default.
* | compatibility with OCaml 4.08David Monniaux2019-09-032-4/+3
| |
* | Fixing upstream merge buildCyril SIX2019-09-031-1/+1
| |
* | aclrw testCyril SIX2019-09-031-0/+12
| |
* | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-03177-6355/+6648
|\ \ | | | | | | | | | | | | | | | | | | Conflicts: configure mppa_k1c/Archi.v mppa_k1c/Asmexpand.ml
| * | macros for fma() fmaf()David Monniaux2019-08-302-0/+3
| | |
| * | fma with first negated operandDavid Monniaux2019-08-303-6/+17
| | |
| * | fmaDavid Monniaux2019-08-3014-15/+166
| | |
| * | début du fmaDavid Monniaux2019-08-304-7/+179
| | |
| * | use finvwDavid Monniaux2019-08-303-4/+45
| | |
| * | add finvw ; not yet generatedDavid Monniaux2019-08-3011-6/+55
| | |
| * | fabsfDavid Monniaux2019-08-293-1/+10
| | |
| * | fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-2912-11/+102
| | |
generated by cgit (git 2.34.1) at 2024-07-11 22:28:53 +0000