aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-03-011-13/+16
|\
| * Check for arguments of struct/union type passed to a vararg functionXavier Leroy2022-02-111-13/+16
* | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-013-8/+2
|\|
| * An improved PTree data structure (#420)Xavier Leroy2021-11-163-8/+2
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-294-7/+7
|\|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-034-7/+7
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-10-041-3/+3
|\|
| * Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-3/+3
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-2419-1623/+3381
|\|
| * 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
* | Commenting out __builtin_expect from AbsIntCyril SIX2021-06-011-2/+2
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-0112-48/+68
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-251/+286
|\|
| * 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
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-186-162/+214
|\|
| * 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
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+9
|\ \
| * | begin installing profilingDavid Monniaux2020-04-081-1/+1
| * | added EF_profilingDavid Monniaux2020-04-081-0/+9
* | | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-099-45/+86
|\ \ \
| * | | expect operationDavid Monniaux2020-04-072-27/+35
| * | | Oexpect in frontendDavid Monniaux2020-04-076-16/+47
| * | | start implementing expect as exprDavid Monniaux2020-04-071-0/+1
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-0611-124/+328
| |\| |
| * | | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-2/+3
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-082-31/+46
|\ \ \ \ | | |/ / | |/| |
| * | | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-2/+2
| |\ \ \ | | | |/ | | |/|
| | * | Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-291-2/+2
| * | | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-29/+44
| |\| |
| | * | Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-29/+44