| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Handle large static initializers for global arrays | Xavier Leroy | 2015-11-09 | 3 | -118/+205 |
| * | Fix for switch was to eager. | Bernhard Schommer | 2015-11-06 | 1 | -6/+8 |
| * | Remove debug stmts during grouping of switch. | Bernhard Schommer | 2015-11-06 | 1 | -3/+5 |
| * | Added printing functions for debug annotations. | Bernhard Schommer | 2015-11-06 | 1 | -0/+3 |
| * | Merge remote-tracking branch 'origin/master' into named-externals | Bernhard Schommer | 2015-10-20 | 1 | -2/+2 |
| |\ |
|
| | * | bug 17392: remove trailing whitespace in source files | Michael Schmidt | 2015-10-14 | 20 | -1989/+1989 |
| | * | bug 17392: remove trailing whitespace in source files | Michael Schmidt | 2015-10-14 | 3 | -41/+41 |
| | * | Unified function for adding the atom identifier. | Bernhard Schommer | 2015-10-12 | 1 | -2/+2 |
| * | | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 23 | -2030/+2030 |
| * | | Use Coq strings instead of idents to name external and builtin functions. | Xavier Leroy | 2015-10-11 | 3 | -14/+15 |
| |/ |
|
| * | Fixed minor issue with parameters that get put on the stack, made | Bernhard Schommer | 2015-09-30 | 1 | -4/+6 |
| * | Added location for the formal parameters and move the end of all | Bernhard Schommer | 2015-09-28 | 1 | -0/+1 |
| * | Merge branch 'debugscopes' into debug_locations | Bernhard Schommer | 2015-09-21 | 2 | -41/+39 |
| |\ |
|
| | * | Experiment: track the scopes of local variables via __builtin_debug. | Xavier Leroy | 2015-09-20 | 1 | -38/+36 |
| | * | Ctypes.composite_of_def: make sure it computes within Coq. | Xavier Leroy | 2015-09-18 | 1 | -3/+3 |
| * | | Started implementing the scope for the Debug Informations. | Bernhard Schommer | 2015-09-18 | 1 | -0/+1 |
| * | | First version with computation of dwarf info from debug info. | Bernhard Schommer | 2015-09-17 | 1 | -1/+1 |
| * | | Move more functionality in the new interface. | Bernhard Schommer | 2015-09-16 | 1 | -4/+7 |
| * | | X | Bernhard Schommer | 2015-09-06 | 4 | -77/+215 |
| |\| |
|
| | * | 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 |
| * | | Added symbol functions for printing of the location for global variables. | Bernhard Schommer | 2015-08-21 | 1 | -2/+8 |
| |/ |
|
| * | 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 |
