aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | |
| | * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-058-23/+22
| | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
| | * Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-051-17/+3
| | | | | | | | | | | | PG now uses the _Coqproject file and finds relevant paths there.
| * | various fixesDavid Monniaux2019-07-1910-31/+28
| | |
| * | helpers broke compilationDavid Monniaux2019-07-1914-67/+68
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-19122-4300/+5853
| |\| | | | | | | | | | mppa-work-upstream-merge
| | * Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
| | | | | | | | | | | | | | | It supports a branch-free implementation of floatofintu. Not used yet in any of the ports.
| | * x86_64: branchless implementation of floatofintu and intuoffloatXavier Leroy2019-07-172-14/+29
| | | | | | | | | | | | | | | | | | | | | The implementation uses float <-> signed 64-bit integer conversion instructions, and is both efficient and branchless. Based on a suggestion by Rémi Hutin.
| | * When testing builtin functions, prevent constant propagationXavier Leroy2019-07-174-28/+31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that some builtin functions have known semantics, constant propagation can happen in this test. This defeats the purpose, which is to check that the correct processor instructions are generated. To prevent this constant propagation, we move the initialized variables to global scope. Since they are not "const", their values are not known to the optimizer.
| | * Make __builtin_sel available from C source codeXavier Leroy2019-07-177-32/+195
| | | | | | | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| | * Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| | | | | | | | | | | | Known built-in functions are guaranteed not to change memory.
| | * Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| | | | | | | | | | | | | | | | | | | | | When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time.
generated by cgit (git 2.34.1) at 2024-07-11 22:43:21 +0000