aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
* Add support for __builtin_fabsfXavier Leroy2020-07-274-0/+13
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-275-12/+0
* More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
* cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
* Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
* Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
* Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
* Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
* Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
* Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
* Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
* Revised detection of menhirLib directory, continued (#365)Xavier Leroy2020-07-151-4/+4
* No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
* Fix typo.Bernhard Schommer2020-07-081-1/+1
* Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
* Use the same version string.Bernhard Schommer2020-07-081-10/+3
* Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
* Introduce additional "branch" build information.Bernhard Schommer2020-07-087-13/+20
* Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
* 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
generated by cgit (git 2.34.1) at 2024-06-28 21:27:41 +0000