| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Avoid `Global Set Asymmetric Patterns` (#408) | Xavier Leroy | 2021-09-15 | 1 | -0/+2 |
| * | Merge branch 'bitfields' (#400) | Xavier Leroy | 2021-08-22 | 19 | -1604/+3295 |
| |\ |
|
| | * | Native support for bit fields (#400) | Xavier Leroy | 2021-08-22 | 19 | -1604/+3243 |
| | * | Add Ctypes.link_match_program_gen | Xavier Leroy | 2021-08-22 | 1 | -0/+52 |
| * | | Revise the declaration of __compcert_* helper functions | Xavier Leroy | 2021-06-30 | 1 | -82/+79 |
| |/ |
|
| * | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 12 | -48/+60 |
| * | Support __builtin_expect | Xavier Leroy | 2021-05-02 | 1 | -0/+5 |
| * | Support __builtin_unreachable | Xavier Leroy | 2021-05-02 | 1 | -0/+3 |
| * | Section handling: finer control of variable initialization | Xavier Leroy | 2021-02-23 | 1 | -1/+6 |
| * | Qualify `Hint` as `Global Hint` where appropriate | Xavier Leroy | 2021-01-21 | 1 | -4/+4 |
| * | Support re-normalization of function parameters at function entry | Xavier Leroy | 2021-01-16 | 2 | -17/+36 |
| * | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 12 | -219/+222 |
| * | Changed cc_varargs to an option type | Bernhard Schommer | 2020-12-25 | 4 | -10/+18 |
| * | Add -main option to specify entrypoint function in interpreter mode (#374) | Xavier Leroy | 2020-10-30 | 1 | -1/+1 |
| * | Add __builtin_sqrt as synonymous for __builtin_fsqrt | Xavier Leroy | 2020-07-27 | 1 | -0/+2 |
| * | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml | Xavier Leroy | 2020-07-27 | 1 | -0/+12 |
| * | Add support for __builtin_fabsf | Xavier Leroy | 2020-07-27 | 1 | -0/+2 |
| * | Move shared code in new file. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| * | Remove the `can_reserve_register` function. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| * | Improve printing of builtin function invocations | Xavier Leroy | 2020-06-25 | 1 | -0/+3 |
| * | SimplExpr: remove unused definition "sd_cast_set" | Xavier Leroy | 2020-06-15 | 1 | -2/+0 |
| * | SimplExpr: better translation of casts in a "for effects" context | Xavier Leroy | 2020-06-15 | 3 | -136/+166 |
| * | Move reserved_registers to CPragmas. | Bernhard Schommer | 2020-04-20 | 1 | -1/+6 |
| * | Explicit error messages for ill-formed section attributes (#232) | Bernhard Schommer | 2020-03-29 | 1 | -2/+2 |
| * | Define the semantics of `free(NULL)` (#226) | Xavier Leroy | 2020-03-02 | 1 | -29/+44 |
| * | Support re-normalization of values returned by function calls | Xavier Leroy | 2020-02-21 | 2 | -33/+137 |
| * | Refine the type of function results in AST.signature | Xavier Leroy | 2020-02-21 | 6 | -39/+78 |
| * | More precise determination of small data accesses (#220) | Bernhard Schommer | 2020-02-20 | 1 | -3/+15 |
| * | Take the sign into account for int to ptr cast. | Bernhard Schommer | 2020-02-12 | 2 | -2/+3 |
| * | Fix for AArch64 alignment problem (#206) | Bernhard Schommer | 2019-11-28 | 1 | -0/+5 |
| * | -dclight output: use nicer names for temporary variables | Xavier Leroy | 2019-09-16 | 1 | -2/+11 |
| * | clightgen -dclight: print function parameters correctly | Xavier Leroy | 2019-09-16 | 2 | -15/+34 |
| * | bswap builtins: give semantics to them, support bswap64 on all targets | Bernhard Schommer | 2019-08-12 | 1 | -1/+3 |
| * | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 4 | -13/+14 |
| * | Make __builtin_sel available from C source code | Xavier Leroy | 2019-07-17 | 5 | -31/+157 |
| * | Give formal semantics to some built-in functions and run-time functions | Xavier Leroy | 2019-07-17 | 1 | -9/+34 |
| * | Remove the cparser/Builtins module | Xavier Leroy | 2019-07-17 | 1 | -7/+10 |
| * | Change the expected types for arguments to __builtin_annot, and extended asm | Xavier Leroy | 2019-06-19 | 1 | -5/+25 |
| * | Fix misspellings in messages, man pages, and comments | Xavier Leroy | 2019-05-31 | 2 | -2/+2 |
| * | Csyntax.v: Fix a typo in a documentation comment (#292) | Bart Jacobs | 2019-05-21 | 1 | -1/+1 |
| * | lib/Coqlib.v: remove defns about multiplication, division, modulus | Xavier Leroy | 2019-04-23 | 2 | -2/+1 |
| * | Replace nat_of_Z with Z.to_nat | Xavier Leroy | 2019-04-23 | 1 | -1/+1 |
| * | Upgrade embedded version of Flocq to 3.1. | Guillaume Melquiond | 2019-03-27 | 1 | -4/+4 |
| * | Distinguish object-related and name-related attributes | Xavier Leroy | 2019-02-25 | 1 | -2/+3 |
| * | Use `Program Instance` instead of `Instance` + refine mode (#261) | Maxime Dénès | 2018-12-27 | 1 | -23/+33 |
| * | Improved diagnostics: spelling, wording, etc (#138) | Michael Schmidt | 2018-09-14 | 1 | -8/+8 |
| * | Attach _Alignas to names and refactor _Alignas checks (#133) | Bernhard Schommer | 2018-09-10 | 1 | -2/+2 |
| * | Import prim token notations before using them | Jason Gross | 2018-08-27 | 3 | -1/+3 |
| * | Issue with packed structs and sizeof, alignof, offsetof in cparser/ | Xavier Leroy | 2018-08-17 | 1 | -1/+3 |
| * | Compatibility with OCaml 4.07 (#241) continued | Xavier Leroy | 2018-07-10 | 1 | -1/+1 |
