aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
* Revise the "bench" entries of the test suiteXavier Leroy2019-09-175-12/+110
* Updates in preparation for release 3.6Xavier Leroy2019-09-162-1/+63
* -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
* clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-163-16/+35
* Reworked json export.Bernhard Schommer2019-09-125-78/+91
* Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-1163-167/+15898
|\
| * AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.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
* | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-052-5/+5
* | Update man page.Bernhard Schommer2019-09-021-1/+1
* | 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
|/
* 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
generated by cgit (git 2.34.1) at 2024-05-20 10:00:02 +0000