aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Second update for release 3.10v3.10Xavier Leroy2021-11-191-4/+6
* mention AArch64 in man-pageMichael Schmidt2021-11-171-1/+1
* Remove documentation of bitfield language support option.Michael Schmidt2021-11-171-5/+0
* First update for release 3.10Xavier Leroy2021-11-163-2/+57
* Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
* An improved PTree data structure (#420)Xavier Leroy2021-11-169-668/+908
* Revised checks for multi-character constants 'xyz'Xavier Leroy2021-11-161-24/+19
* Resurrect a warning for bit fields of enum typesXavier Leroy2021-11-121-15/+33
* PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-284-20/+31
* Explicitly remove __SIZEOF_INT128__ macro definition. (#419)roconnor-blockstream2021-10-161-4/+4
* Merge pull request #415 from AbsInt/coq-8.14-compatXavier Leroy2021-10-1618-58/+68
|\
| * Add Coq 8.14.0 to the supported versions of CoqXavier Leroy2021-10-031-3/+3
| * Selectively turn some Coq 8.14 warnings offXavier Leroy2021-10-031-1/+11
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-0315-53/+53
| * 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
generated by cgit (git 2.34.1) at 2024-05-17 11:13:58 +0000