aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* SimplExpr: better translation of casts in a "for effects" contextXavier Leroy2020-06-153-136/+166
* Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
* Improve portability of the test for annotations inclightgenXavier Leroy2020-06-052-0/+4
* clightgen: fix the printing of annotationsXavier Leroy2020-06-052-59/+14
* clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
* clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
* Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-194-20/+204
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+0
* Update the list of dual-licensed filesXavier Leroy2020-05-051-2/+2
* Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
* Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
* Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
* Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
* Do not use "Declare Scope", introduced in Coq 8.10 onlyXavier Leroy2020-05-041-1/+0
* Coq-MenhirLib: explicit import ListNotations (#354)Jacques-Henri Jourdan2020-05-047-4/+12
* Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-292-1/+19
* Updated .gitignoreBernhard Schommer2020-04-271-0/+1
* Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-204-8/+8
* Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
* Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
* Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
* Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
* 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
generated by cgit (git 2.34.1) at 2024-06-29 03:31:24 +0000