aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Bytecode-only build (#243)Xavier Leroy2020-07-072-4/+29
* Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
* Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
* Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
* Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
* Move shared code in new file.Bernhard Schommer2020-06-2817-96/+46
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-2810-19/+1
* Use library function.Bernhard Schommer2020-06-281-4/+1
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-288-9/+8
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
* Preliminary support for Coq 8.12Xavier Leroy2020-06-212-4/+4
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-213-3/+3
* SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
* 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
generated by cgit (git 2.34.1) at 2024-06-15 03:59:01 +0000