aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* merge upstream including fma fixesDavid Monniaux2019-08-2825-1942/+0
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-2821-63/+102
|\
| * Allow Long as const result for ppc64 variant.Bernhard Schommer2019-08-132-0/+3
| * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-126-7/+51
| * x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-061-13/+19
| * Add support for Coq 8.10Xavier Leroy2019-08-051-2/+2
| * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
| * 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
| * Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-051-17/+3
* | 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 mppa-work-up...David Monniaux2019-07-19122-4300/+5853
|\|
| * Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
| * x86_64: branchless implementation of floatofintu and intuoffloatXavier Leroy2019-07-172-14/+29
| * When testing builtin functions, prevent constant propagationXavier Leroy2019-07-174-28/+31
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-177-32/+195
| * Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| * Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-1720-187/+1154
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-1719-104/+82
| * Add floating-point square root and fused multiply-addXavier Leroy2019-07-176-3/+76
| * Add FMA (fused multiply-add)Xavier Leroy2019-07-171-0/+121
| * Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
| * Revised specification of NaN payload behaviorXavier Leroy2019-07-126-193/+209
| * More precise description of '-O0' and 'non-linear-cond-expr'Michael Schmidt2019-07-101-1/+2
| * Change condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| * -O0 now implies -fno-inliningMichael Schmidt2019-07-091-1/+1
| * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-089-12/+11
| * Make configure resistant to Windows EOL and paths (#305)MSoegtropIMC2019-07-081-1/+1
| * Fix compatibility with Coq 8.10 (#303)Jacques-Henri Jourdan2019-07-063-9/+10
| * Update synonymous list for -O0, add new named warning classMichael Schmidt2019-07-051-1/+6
| * Update documentation of -ObranchlessXavier Leroy2019-07-052-7/+9
| * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-053-7/+7
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0534-3583/+3163
| * Avoid relying on `Export` bug (#301)Maxime Dénès2019-07-041-1/+2
| * Deref is not safe.Bernhard Schommer2019-07-041-1/+1
| * Added new diagnostic for non-linear conditionalsBernhard Schommer2019-07-046-1/+179
| * Added helper function for array types.Bernhard Schommer2019-07-042-0/+7
| * Added statement traversal functions.Bernhard Schommer2019-07-041-107/+90
| * Change the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
| * Extended asm: print register names according to their typesXavier Leroy2019-06-176-19/+34
| * Updated man page.Bernhard Schommer2019-06-171-0/+10
| * Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-177-6/+128
* | Fixing the generation of verifier_times.txt and oracle_times.txtCyril SIX2019-07-182-7/+7
* | Removing a hidden FIXME that hopefully didn't have any impact..Cyril SIX2019-07-181-7/+0
* | (#137) Removed the useless strings in PostpassSchedulingOracleCyril SIX2019-07-181-337/+254
* | Typo in PrevsubxwCyril SIX2019-07-181-1/+1
* | (#142) Desactivating scheduling when using -O1 optimizationCyril SIX2019-07-172-2/+4
* | Merge branch 'paper-artefact' into mppa-workCyril SIX2019-07-171-27/+27
|\ \
generated by cgit (git 2.34.1) at 2024-07-12 04:31:04 +0000