| Commit message (Expand) | Author | Age | Files | Lines |
* | 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 |
* | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 1 | -89/+92 |
* | Merge of the clightgen branch: | xleroy | 2012-12-29 | 1 | -2/+1 |
* | Support for inline assembly (asm statements). | xleroy | 2012-12-18 | 1 | -0/+7 |
* | Make Clight independent of CompCert C. | xleroy | 2012-10-08 | 1 | -0/+2 |
* | Merge of branch seq-and-or. See Changelog for details. | xleroy | 2012-10-06 | 1 | -1/+114 |
* | - Revised non-overflow constraints on memory injections so that | xleroy | 2012-07-23 | 1 | -3/+4 |
* | Revert unintentional commit #1955 | xleroy | 2012-07-06 | 1 | -7/+0 |