aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
* | | 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
|\ \ \
| * | | 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 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
generated by cgit (git 2.34.1) at 2024-06-13 10:33:33 +0000