aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* 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
* Remove duplicated ticks.Bernhard Schommer2019-10-011-2/+2
* Use pointer type for evaluated constants.Bernhard Schommer2019-10-011-1/+1
* Various improvements for diagnostics.Bernhard Schommer2019-09-303-10/+34
* Added .gitattributes file.Bernhard Schommer2019-09-301-0/+3
* Functions that are extern should stay extern (#201)Bernhard Schommer2019-09-251-1/+1
* Model GPR0 in isel (#199)Xavier Leroy2019-09-172-2/+4
* 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
generated by cgit (git 2.34.1) at 2024-06-18 12:07:58 +0000