| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-work | Cyril SIX | 2020-04-01 | 1 | -2/+2 |
| |\ |
|
| | * | Explicit error messages for ill-formed section attributes (#232) | Bernhard Schommer | 2020-03-29 | 1 | -2/+2 |
| * | | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 1 | -29/+44 |
| |\| |
|
| | * | Define the semantics of `free(NULL)` (#226) | Xavier Leroy | 2020-03-02 | 1 | -29/+44 |
| * | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 1 | -4/+36 |
| |\ \
| |/
|/| |
|
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-12-09 | 1 | -0/+5 |
| | |\ |
|
| | * \ | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea... | David Monniaux | 2019-09-20 | 2 | -17/+45 |
| | |\ \ |
|
| | * \ \ | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-08-28 | 5 | -14/+17 |
| | |\ \ \ |
|
| | * \ \ \ | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-07-19 | 6 | -65/+227 |
| | |\ \ \ \ |
|
| | * \ \ \ \ | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-... | David Monniaux | 2019-06-03 | 6 | -10/+9 |
| | |\ \ \ \ \ |
|
| | * | | | | | | ternary ops for float/double | David Monniaux | 2019-04-03 | 1 | -0/+4 |
| | * | | | | | | problem in ValueAOp | David Monniaux | 2019-04-03 | 1 | -0/+1 |
| | * | | | | | | attempts at generating builtins, start | David Monniaux | 2019-04-03 | 1 | -1/+8 |
| | * | | | | | | la division flottante fonctionne | David Monniaux | 2019-03-20 | 1 | -2/+16 |
| | * | | | | | | ça semble passer | David Monniaux | 2019-03-20 | 1 | -2/+4 |
| | * | | | | | | added helper functions but strange | David Monniaux | 2019-03-19 | 1 | -1/+17 |
| * | | | | | | | 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 |
| * | String literals are l-values and have array types (#116) | Bernhard Schommer | 2018-05-27 | 1 | -6/+7 |
| * | Record value of constant expression in C.Scase constructor | Xavier Leroy | 2018-04-27 | 1 | -1/+1 |
| * | Warn when volatile struct is assigned to a normal struct | Bernhard Schommer | 2018-04-19 | 1 | -0/+3 |
| * | Print size argument of Init_space as Z not as int32 | Xavier Leroy | 2018-03-13 | 1 | -1/+1 |
| * | Do not use "Require" inside sections (#224) | Xavier Leroy | 2018-03-12 | 1 | -2/+1 |
| * | Improve and simplify error messages. | Bernhard Schommer | 2018-03-07 | 1 | -5/+1 |
| * | Reactivated and improved ais annotations. | Bernhard Schommer | 2018-03-06 | 1 | -24/+35 |
| * | Truncation of array sizes when converting them to Coq's Z type | Xavier Leroy | 2018-02-08 | 1 | -6/+8 |
| * | Refactor the handling of errors and warnings (#44) | Bernhard Schommer | 2018-02-08 | 2 | -17/+20 |
