aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Completely avoid line breaks in types when printing error messagesXavier Leroy2022-05-071-6/+10
* Enum is only compatible with IInt.Xavier Leroy2022-05-061-4/+4
* Merge pull request #368 from silene/flocq-3.4Xavier Leroy2022-04-2938-2934/+5149
|\
| * Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-2611-285/+737
| * Support Coq 8.15.1Xavier Leroy2022-04-251-2/+2
| * Make Coq 8.12.0 the minimal version.Guillaume Melquiond2022-04-251-2/+2
| * Ignore .coq-native directories.Guillaume Melquiond2022-04-251-0/+1
| * Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-2536-2875/+4637
|/
* Fix a typo in a comment in Clight.v (#427)Hanzhi Liu2022-04-251-1/+1
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-257-9/+31
* Check for arguments of struct/union type passed to a vararg functionXavier Leroy2022-02-111-13/+16
* Add op for float max and min for x86.Bernhard Schommer2022-02-0710-23/+66
* Return second arg for float min/max on x86.Bernhard Schommer2022-02-071-4/+4
* Support Coq 8.15.0Xavier Leroy2022-01-311-2/+2
* Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-103-6/+6
* Fix pattern for github-linguist.Bernhard Schommer2021-12-141-2/+2
* Enforce evaluation order in IRC.add_interf and IRC.add_prefXavier Leroy2021-12-071-2/+2
* Support Coq 8.14.1Xavier Leroy2021-11-261-2/+2
* 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
generated by cgit (git 2.34.1) at 2024-05-09 14:20:05 +0000