aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}aarch64xavier.leroy2019-08-312-4/+4
* Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-176-16/+16
* Test for the compilation of floating-point literalsXavier Leroy2019-08-083-1/+562
* AArch64 portXavier Leroy2019-08-0848-87/+14874
* Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
* Factor out endianness determination between testsXavier Leroy2019-08-074-30/+14
* ndfun: add support for guards on patternsXavier Leroy2019-08-071-5/+16
* More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
* Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
* Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
* Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
* Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
* Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
* x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-071-13/+19
* Add support for Coq 8.10Xavier Leroy2019-08-071-2/+2
* Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-071-0/+1
* Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-078-23/+22
* Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-071-17/+3
* 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
generated by cgit (git 2.34.1) at 2024-05-02 15:06:58 +0000