aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Updates for release 3.7v3.7Xavier Leroy2020-03-311-1/+1
* Updates for release 3.7Xavier Leroy2020-03-312-1/+6
* Update ChangelogXavier Leroy2020-03-311-3/+34
* Double rounding error in int64->float32 conversions on PowerPC and ARMXavier Leroy2020-03-304-24/+22
* Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
* Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-293-12/+25
* Include typedef name in error message (#228)Bernhard Schommer2020-03-041-2/+2
* Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
* Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-022-43/+74
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-022-18/+35
* Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
* In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
* Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
* Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
* The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-247-649/+68
* AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-215-6/+6
* Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
* Support re-normalization of values returned by function callsXavier Leroy2020-02-217-33/+174
* Refine the type of function results in AST.signatureXavier Leroy2020-02-2143-286/+445
* More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
* Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
* Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
* Added base address if needed.Bernhard Schommer2020-02-063-33/+53
* Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-063-7/+7
* Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-053-5/+9
* Support Coq 8.11.0 (#212)Xavier Leroy2020-02-054-2/+8
* Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
* Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
* Remove __builtin_nop from list of x86 builtins.Bernhard Schommer2020-01-031-3/+0
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-0314-3/+33
* Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-2114-33/+3
* The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
* Allow Coq 8.10.2.Bernhard Schommer2019-12-031-1/+1
* Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-284-2/+13
* Added dwarf register numbers for aarch64Bernhard Schommer2019-11-281-3/+18
* Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
* Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
* Raise minimal required versions for OCaml and Coq (#203)Bernhard Schommer2019-10-311-9/+4
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
* Add support for Coq 8.10.1Xavier Leroy2019-10-281-2/+2
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-282-4/+16
* Fix configure for coq 8.10.0Michael Schmidt2019-10-131-2/+2
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-024-15/+17