aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
|\ \
| * | (#107) Rename "forward_simu" into "bisimu"Cyril SIX2019-07-171-27/+27
* | | README fileCyril SIX2019-07-171-60/+67
* | | rules.mk adding more customizationCyril SIX2019-07-171-3/+3
* | | Portage réussi et completCyril SIX2019-07-175-14/+14
* | | Removing the genmake.py and the generate_makefiles.shCyril SIX2019-07-172-147/+0
* | | All working benches portedCyril SIX2019-07-1728-49/+53
* | | Up to nttCyril SIX2019-07-1712-15/+20
* | | bitsliced-teaCyril SIX2019-07-175-24/+11
* | | bitsliced-aes doneCyril SIX2019-07-174-3275/+7
* | | (#141) Started to port the new Makefile to rules.mk. Ported binary_searchCyril SIX2019-07-173-57/+144
* | | Deleting junk filesCyril SIX2019-07-177-1932/+0