aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Fix a comment in Cstrategy.v (#485)Xuyang Li2023-04-051-2/+2
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-101-2/+2
* Don't discard argument of `__builtin_va_end`Michael Schmidt2023-01-231-2/+2
* C2C: wrong handling of typedefs to enums in bit fieldsXavier Leroy2023-01-231-1/+1
* Fix incomplete checking of unsolved holes (#465)Gaëtan Gilbert2022-11-281-1/+1
* Merge pull request #459 from AbsInt/full-switchXavier Leroy2022-11-091-84/+18
|\
| * Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-291-84/+18
* | SimplExpr: revised handling of nested conditional, `||`, `&&` operatorsXavier Leroy2022-10-013-98/+165
|/
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-191-102/+95
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-192-0/+7
* Rework of struct member offsets for debug info.Bernhard Schommer2022-09-031-12/+45
* Introduce `struct_layout` functionBernhard Schommer2022-09-031-0/+26
* Support mergeable sections for string literals and wide string literalsXavier Leroy2022-08-291-6/+13
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-291-2/+2
* Fix a typo in a comment in Clight.v (#427)Hanzhi Liu2022-04-251-1/+1
* Check for arguments of struct/union type passed to a vararg functionXavier Leroy2022-02-111-13/+16
* An improved PTree data structure (#420)Xavier Leroy2021-11-163-8/+2
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-034-7/+7
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-3/+3
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-0/+2
* Merge branch 'bitfields' (#400)Xavier Leroy2021-08-2219-1604/+3295
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-2219-1604/+3243
| * Add Ctypes.link_match_program_genXavier Leroy2021-08-221-0/+52
* | Revise the declaration of __compcert_* helper functionsXavier Leroy2021-06-301-82/+79
|/
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0812-48/+60
* Support __builtin_expectXavier Leroy2021-05-021-0/+5
* Support __builtin_unreachableXavier Leroy2021-05-021-0/+3
* Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+6
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-4/+4
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-162-17/+36
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-219/+222
* Changed cc_varargs to an option typeBernhard Schommer2020-12-254-10/+18
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-1/+1
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+2
* Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-0/+12
* Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+2
* Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-281-1/+1
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+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
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-1/+6
* Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-291-2/+2
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-29/+44
* Support re-normalization of values returned by function callsXavier Leroy2020-02-212-33/+137
* Refine the type of function results in AST.signatureXavier Leroy2020-02-216-39/+78
* More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
* Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
* Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-0/+5
* -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
generated by cgit (git 2.34.1) at 2024-05-04 03:29:35 +0000