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
* | | Englishification of commentsCyril SIX2019-09-032-11/+6
* | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-08-3129-689/+435
|\ \ \
| * | | Rajout de clzd dans les testsCyril SIX2019-08-302-3/+5
| * | | Added more testsCyril SIX2019-08-305-29/+58
| * | | (#157) Removed AFADDD and AFADDW from the builtinsCyril SIX2019-08-306-9/+22
| * | | Adding tests for addx8d addx8w etc..Cyril SIX2019-08-303-2/+11