| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-24 | 1 | -130/+192 |
| |\ |
|
| | * | Native support for bit fields (#400) | Xavier Leroy | 2021-08-22 | 1 | -130/+192 |
| * | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -5/+5 |
| |\| |
|
| | * | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 1 | -5/+5 |
| * | | begin installing profiling | David Monniaux | 2020-04-08 | 1 | -1/+1 |
| * | | added EF_profiling | David Monniaux | 2020-04-08 | 1 | -0/+9 |
| |/ |
|
| * | Define the semantics of `free(NULL)` (#226) | Xavier Leroy | 2020-03-02 | 1 | -29/+44 |
| * | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 1 | -5/+6 |
| * | Give formal semantics to some built-in functions and run-time functions | Xavier Leroy | 2019-07-17 | 1 | -9/+34 |
| * | lib/Coqlib.v: remove defns about multiplication, division, modulus | Xavier Leroy | 2019-04-23 | 1 | -1/+0 |
| * | Merge pull request #191 from sigurdschneider/master | Xavier Leroy | 2017-10-20 | 1 | -0/+1 |
| |\ |
|
| | * | Ensure FunInd or Recdef is imported if functional induction is used | Sigurd Schneider | 2017-07-20 | 1 | -0/+1 |
| * | | New support for inserting ais-annotations. | Bernhard Schommer | 2017-10-19 | 1 | -2/+2 |
| * | | Remove coq warnings (#28) | Bernhard Schommer | 2017-09-22 | 1 | -1/+1 |
| |/ |
|
| * | Some backward compatible Ltac fixes, necessary for 8.6. | Maxime Dénès | 2017-01-09 | 1 | -5/+7 |
| * | Support for 64-bit architectures: generic support | Xavier Leroy | 2016-10-01 | 1 | -118/+119 |
| * | Merge pull request #142 from maximedenes/minor-fixes | Xavier Leroy | 2016-09-21 | 1 | -5/+8 |
| |\ |
|
| | * | Fix minor issues in some proofs and tactics. | Maxime Dénès | 2016-09-21 | 1 | -5/+8 |
| * | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy | Xavier Leroy | 2016-09-17 | 1 | -31/+4 |
| |/ |
|
| * | Merge pull request #93 from AbsInt/separate-compilation | Xavier Leroy | 2016-03-20 | 1 | -0/+5 |
| |\ |
|
| | * | Add support for EF_runtime externals | Xavier Leroy | 2016-03-06 | 1 | -0/+5 |
| * | | Make casts of pointers to _Bool semantically well defined (again). | Xavier Leroy | 2016-03-02 | 1 | -29/+29 |
| |/ |
|
| * | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 1 | -134/+134 |
| * | Use Coq strings instead of idents to name external and builtin functions. | Xavier Leroy | 2015-10-11 | 1 | -4/+4 |
| * | Refactoring of builtins and annotations in the back-end. | Xavier Leroy | 2015-08-21 | 1 | -50/+20 |
| * | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 1 | -1/+1 |
| * | Experiment: support a subset of GCC's extended asm statements. | Xavier Leroy | 2015-04-17 | 1 | -8/+8 |
| * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 1 | -3/+3 |
| |\ |
|
| | * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 1 | -3/+3 |
| * | | Omission: forgot to treat pointer values in bool_of_val and sem_notbool. | Xavier Leroy | 2015-03-29 | 1 | -16/+16 |
| |/ |
|
| * | Interpreter produces more detailed trace, including name of semantic rules used. | Xavier Leroy | 2015-02-08 | 1 | -135/+164 |
| * | Represent struct and union types by name instead of by structure. | Xavier Leroy | 2014-12-22 | 1 | -38/+42 |
| * | Introduce symbol environments (type Senv.t) as a restricted view on global en... | Xavier Leroy | 2014-11-26 | 1 | -12/+12 |
| * | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 1 | -7/+15 |
| * | Revised translation of '&&' and '||' to Clight. | Xavier Leroy | 2014-10-13 | 1 | -10/+10 |
| * | - Support "switch" statements over 64-bit integers | xleroy | 2014-08-17 | 1 | -5/+3 |
| * | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 1 | -14/+5 |
| * | Continued: change typeconv t into incrdecr_type t for Epostincr. | xleroy | 2014-04-16 | 1 | -1/+1 |
| * | Remove useless checks on type_of_global in dynamic semantics | xleroy | 2014-02-20 | 1 | -7/+3 |
| * | Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union). | xleroy | 2013-12-30 | 1 | -5/+10 |
| * | Simpler, more robust emulation of calls to variadic functions: | xleroy | 2013-12-28 | 1 | -11/+11 |
| * | Merge of branch value-analysis. | xleroy | 2013-12-20 | 1 | -1/+1 |
| * | Revised semantics of external functions, continued: | xleroy | 2013-11-18 | 1 | -35/+36 |
| * | Revised modeling of external functions and built-in functions: just axiomatize | xleroy | 2013-11-17 | 1 | -17/+18 |
| * | Revised treatment of _Alignas, for better compatibility with GCC and Clang, a... | xleroy | 2013-11-06 | 1 | -2/+1 |
| * | Merge of the "alignas" branch. | xleroy | 2013-10-05 | 1 | -4/+5 |
| * | Merge of the float32 branch: | xleroy | 2013-05-19 | 1 | -1/+6 |
| * | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 1 | -0/+4 |
| * | Glasnost: making transparent a number of definitions that were opaque | xleroy | 2013-03-10 | 1 | -4/+3 |
| * | Constant propagation within __builtin_annot. | xleroy | 2013-02-24 | 1 | -4/+5 |
