| Commit message (Expand) | Author | Age | Files | Lines |
* | Ctypes.composite_of_def: make sure it computes within Coq. | Xavier Leroy | 2015-09-18 | 1 | -3/+3 |
* | Track the locations of local variables using EF_debug annotations. | Xavier Leroy | 2015-08-23 | 2 | -26/+194 |
* | Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. | Xavier Leroy | 2015-08-22 | 1 | -1/+1 |
* | Refactoring of builtins and annotations in the back-end. | Xavier Leroy | 2015-08-21 | 1 | -50/+20 |
* | Tighten and prove correct the underflow/overflow bounds for parsing of FP lit... | Xavier Leroy | 2015-07-06 | 1 | -41/+29 |
* | Added a fast test for too large exponents too avoid never ending computations. | Bernhard Schommer | 2015-07-03 | 1 | -29/+42 |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert | Xavier Leroy | 2015-06-30 | 1 | -1/+26 |
|\ |
|
| * | Check also the discarded part of the switch statements for cases outside of a... | Bernhard Schommer | 2015-06-26 | 1 | -1/+26 |
* | | Signedness issue in specification of subtraction between two pointers. | Xavier Leroy | 2015-06-30 | 3 | -6/+19 |
|/ |
|
* | In AST.calling_conventions, record whether the original C function was "old-s... | Xavier Leroy | 2015-05-22 | 3 | -20/+24 |
* | Missing case in type_conditional (long long vs. int or float). | Xavier Leroy | 2015-05-22 | 1 | -6/+3 |
* | Ctyping: better typing of conditional expressions. | Xavier Leroy | 2015-05-21 | 3 | -50/+200 |
* | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 2 | -3/+3 |
* | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va... | Xavier Leroy | 2015-04-30 | 4 | -80/+80 |
* | Warn if a nonzero FP literal converts to infinity (overflow) or to 0 (underfl... | Xavier Leroy | 2015-04-25 | 1 | -3/+17 |
* | Use Cerrors for error reporting instead of rolling our own reporting in C2C. | Xavier Leroy | 2015-04-21 | 1 | -11/+5 |
* | Printing of EF_inline_asm builtins in GCC extended asm syntax. | Xavier Leroy | 2015-04-21 | 1 | -0/+30 |
* | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 2 | -81/+16 |
* | Experiment: support a subset of GCC's extended asm statements. | Xavier Leroy | 2015-04-17 | 2 | -10/+101 |
* | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 2 | -5/+4 |
|\ |
|
| * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 1 | -2/+1 |
| * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 1 | -3/+3 |
* | | Merge pull request #31 from AbsInt/null-ptr-cmp | Xavier Leroy | 2015-04-01 | 13 | -128/+182 |
|\ \ |
|
| * | | Omission: forgot to treat pointer values in bool_of_val and sem_notbool. | Xavier Leroy | 2015-03-29 | 12 | -120/+182 |
| * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 4 | -8/+0 |
| |/ |
|
* | | Fix overflows in printers for clight and csyntax. | Jacques-Henri Jourdan | 2015-04-01 | 2 | -2/+2 |
* | | Support va_arg for vararg arguments of composite (struct/union) types. | Xavier Leroy | 2015-03-20 | 1 | -13/+37 |
|/ |
|
* | Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their typ... | Xavier Leroy | 2015-03-10 | 1 | -1/+3 |
* | Interpreter produces more detailed trace, including name of semantic rules used. | Xavier Leroy | 2015-02-08 | 2 | -136/+165 |
* | Merge branch 'named-structs' | Xavier Leroy | 2015-01-23 | 21 | -1418/+3717 |
|\ |
|
| * | Define a nonnegative integer "rank" for types to support structural induction... | Xavier Leroy | 2015-01-10 | 2 | -22/+120 |
| * | Add a type system for CompCert C and type-checking constructor functions. | Xavier Leroy | 2014-12-31 | 2 | -64/+2079 |
| * | Represent struct and union types by name instead of by structure. | Xavier Leroy | 2014-12-22 | 20 | -1308/+1518 |
| * | Introduce symbol environments (type Senv.t) as a restricted view on global en... | Xavier Leroy | 2014-11-26 | 3 | -44/+20 |
* | | Delay reads from !Machine.config before it is properly initialized. | Xavier Leroy | 2015-01-22 | 1 | -2/+2 |
* | | Protect against redefinition of the __i64_xxx helper library functions. | Xavier Leroy | 2015-01-20 | 1 | -1/+54 |
* | | PR#19: there is no reason to reject an empty "switch" statement. | Xavier Leroy | 2015-01-06 | 1 | -2/+0 |
* | | PR#15: vararg functions are not eligible for inlining. | Xavier Leroy | 2015-01-02 | 1 | -1/+1 |
* | | Translation of wide string literals. | Xavier Leroy | 2015-01-01 | 1 | -6/+57 |
|/ |
|
* | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 5 | -22/+51 |
* | Record public global definitions via field "prog_public" in AST.program. | Xavier Leroy | 2014-11-24 | 3 | -59/+68 |
* | Revised translation of '&&' and '||' to Clight. | Xavier Leroy | 2014-10-13 | 10 | -123/+108 |
* | Tolerance in parsing of 'section' pragma | xleroy | 2014-09-17 | 1 | -0/+3 |
* | More careful detection of inlined builtins. Produces better error messages i... | xleroy | 2014-08-25 | 1 | -0/+1 |
* | Support C99 compound literals (by expansion in Unblock pass). | xleroy | 2014-08-21 | 1 | -0/+2 |
* | Issue with switch labels that are negative 32-bit integers. | xleroy | 2014-08-17 | 1 | -4/+7 |
* | - Support "switch" statements over 64-bit integers | xleroy | 2014-08-17 | 15 | -57/+102 |
* | All targets: add __builtin_membar | xleroy | 2014-07-28 | 1 | -0/+5 |
* | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 18 | -249/+460 |
* | Cleaner, more resilient parsing of pragmas. | xleroy | 2014-06-05 | 1 | -55/+25 |