aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Vendored Flocq library: address Coq 8.14 warningXavier Leroy2021-10-031-1/+1
* Synchronize vendored MenhirLib with upstream (#416)Jacques-Henri Jourdan2021-10-037-36/+47
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-032-4/+4
* Typo in expand_builtin_memcpy_smallXavier Leroy2021-10-011-1/+1
* Ignore unnamed bit fields for initialization of unionsBernhard Schommer2021-09-282-7/+16
* Ignore unnamed plain members of structs and unionsXavier Leroy2021-09-281-10/+15
* Merge pull request #413 from AbsInt/new-exportXavier Leroy2021-09-2727-694/+1098
|\
| * Update export/README.mdXavier Leroy2021-09-221-18/+18
| * Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-2221-271/+625
| * Refactor clightgenXavier Leroy2021-09-2213-594/+644
* | Vendored MenhirLib: replace Require Omega with Require ZArithXavier Leroy2021-09-251-1/+1
* | Update the vendored Flocq library to version 3.4.2Xavier Leroy2021-09-255-38/+24
* | Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-234-8/+8
* | For __builtin_memcpy_aligned, watch out for alignment of stack offsetsXavier Leroy2021-09-231-0/+1
|/
* Fix the type and the semantics of BI_bselXavier Leroy2021-09-221-4/+17
* For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-158-5/+13
* clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-152-16/+28
* Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-132-4/+4
* Share code for memory access for PowerPCBernhard Schommer2021-09-064-166/+159
* Protect against overflows in `leaq` (all forms)Bernhard Schommer2021-08-271-22/+27
* Protect against overflows in `leaq N(src), dst` (#407)Xavier Leroy2021-08-271-12/+17
* Merge branch 'bitfields' (#400)Xavier Leroy2021-08-2245-2305/+4004
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-2242-2299/+3866
| * Add Ctypes.link_match_program_genXavier Leroy2021-08-221-0/+52
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-223-6/+6
| * Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
| * More lemmas about `align`Xavier Leroy2021-07-261-0/+17
| * More lemmas about list appendXavier Leroy2021-07-261-0/+26
* | Revise the declaration of __compcert_* helper functionsXavier Leroy2021-06-301-82/+79
* | x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
* | Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
|/
* Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
* Update for release 3.9v3.9Xavier Leroy2021-05-101-1/+1
* Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
* Update for release 3.9Xavier Leroy2021-05-091-4/+5
* Update ChangelogXavier Leroy2021-05-081-1/+11
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
* Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
* Support __builtin_expectXavier Leroy2021-05-021-0/+5
* Support __builtin_unreachableXavier Leroy2021-05-028-2/+32
* Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
* Update ChangelogXavier Leroy2021-04-291-0/+53
* Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
* MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
* Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
* More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
* Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
* Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
* Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
generated by cgit (git 2.34.1) at 2024-07-01 03:31:53 +0000