aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | |
| * | begin implementing minf/maxfDavid Monniaux2019-08-295-11/+128
| | |
| * | merge upstream including fma fixesDavid Monniaux2019-08-2825-1942/+0
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-2821-63/+102
| |\| | | | | | | | | | mppa-work-upstream-merge
| | * Allow Long as const result for ppc64 variant.Bernhard Schommer2019-08-132-0/+3
| | | | | | | | | | | | Since the ppc64 has 64 bit registers it is okay to have a 64 bit constant result.
| | * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-126-7/+51
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
| | * x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-061-13/+19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a misunderstanding on the asm syntax for 3-operand instructions such as vfmadd132: when the Intel manual reads vfmadd132 res, arg2, arg3 the corresponding GNU asm syntax is vfmadd132 arg3, arg2, res but not vfmadd132 arg2, arg3, res Closes: #188
| | * Add support for Coq 8.10Xavier Leroy2019-08-051-2/+2
| | |
| | * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The "undeclared-scope" warning fires when we use a "notation" scope before having declared it. This is a good thing, except that the "Declare Scope" vernacular that declares a scope was introduced in Coq 8.10 and is not available in earlier versions. Hence there is no way to avoid triggering the warning yet remain compatible with pre-8.10 Coq versions. This commit silences the warning. It will have to revisited when Coq 8.10 is the oldest version of Coq we support in CompCert.
| | * Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-051-1/+1
| | |
generated by cgit (git 2.34.1) at 2024-07-12 03:40:51 +0000