| Commit message (Expand) | Author | Age | Files | Lines |
* | Added missing , in PrintCsyntax. Bug 19599 | Bernhard Schommer | 2016-08-22 | 1 | -1/+1 |
* | fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can... | Michael Schmidt | 2016-06-07 | 1 | -1/+1 |
* | Introduce register pairs to describe calling conventions more precisely | Xavier Leroy | 2016-05-17 | 1 | -2/+2 |
* | Merge branch 'master' into cleanup | Bernhard Schommer | 2016-03-21 | 1 | -7/+9 |
|\ |
|
| * | Merge pull request #93 from AbsInt/separate-compilation | Xavier Leroy | 2016-03-20 | 1 | -1/+3 |
| |\ |
|
| | * | Add support for EF_runtime externals | Xavier Leroy | 2016-03-06 | 1 | -1/+3 |
| * | | Print floating-point numbers with more digits in debug outputs | Xavier Leroy | 2016-03-15 | 1 | -4/+4 |
| |/ |
|
* | | Deactivate warning 27 and added back removed code. | Bernhard Schommer | 2016-03-15 | 1 | -7/+7 |
* | | Code cleanup. | Bernhard Schommer | 2016-03-10 | 1 | -16/+13 |
|/ |
|
* | Added printing functions for debug annotations. | Bernhard Schommer | 2015-11-06 | 1 | -0/+3 |
* | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 1 | -2/+2 |
* | Use Coq strings instead of idents to name external and builtin functions. | Xavier Leroy | 2015-10-11 | 1 | -4/+4 |
* | In AST.calling_conventions, record whether the original C function was "old-s... | Xavier Leroy | 2015-05-22 | 1 | -1/+1 |
* | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 1 | -2/+2 |
* | Printing of EF_inline_asm builtins in GCC extended asm syntax. | Xavier Leroy | 2015-04-21 | 1 | -0/+30 |
* | Fix overflows in printers for clight and csyntax. | Jacques-Henri Jourdan | 2015-04-01 | 1 | -1/+1 |
* | Represent struct and union types by name instead of by structure. | Xavier Leroy | 2014-12-22 | 1 | -122/+19 |
* | Revised translation of '&&' and '||' to Clight. | Xavier Leroy | 2014-10-13 | 1 | -2/+2 |
* | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 1 | -0/+2 |
* | Beautify the output. | xleroy | 2014-02-21 | 1 | -3/+7 |
* | Better printing of integer literals: add U and LL suffixes when needed. | xleroy | 2014-01-12 | 1 | -9/+22 |
* | Simpler, more robust emulation of calls to variadic functions: | xleroy | 2013-12-28 | 1 | -26/+24 |
* | Support "default" cases in the middle of a "switch", not just at the end. | xleroy | 2013-12-21 | 1 | -11/+13 |
* | Cleaner printing of global variables. | xleroy | 2013-11-09 | 1 | -21/+30 |
* | - Recognize __builtin_fabs as an operator, not just a builtin, | xleroy | 2013-11-06 | 1 | -0/+3 |
* | Merge of the "alignas" branch. | xleroy | 2013-10-05 | 1 | -1/+5 |
* | Preliminary support for debugging info (-g). | xleroy | 2013-05-17 | 1 | -4/+4 |
* | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 1 | -0/+10 |
* | Watch out for behaviors exponential in the nesting of struct/union types. | xleroy | 2013-03-23 | 1 | -15/+13 |
* | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 1 | -1/+1 |
* | Globalenvs: allocate one-byte block with permissions Nonempty for each | xleroy | 2012-11-12 | 1 | -13/+14 |
* | 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/+22 |
* | Forgot to collect types of expressions | xleroy | 2012-07-28 | 1 | -1/+3 |
* | Use Flocq for floats | xleroy | 2012-06-28 | 1 | -3/+3 |
* | Better printing of pointer values and of locations. | xleroy | 2012-02-29 | 1 | -10/+16 |
* | - Support for _Alignof(ty) operator from ISO C 2011 | xleroy | 2012-02-26 | 1 | -1/+5 |
* | Don't print external declarations for builtins. | xleroy | 2012-02-18 | 1 | -2/+4 |
* | Merge of the "volatile" branch: | xleroy | 2012-02-04 | 1 | -23/+32 |
* | Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars | xleroy | 2011-10-18 | 1 | -8/+8 |
* | Added animation of the CompCert C semantics (ccomp -interp) | xleroy | 2011-07-28 | 1 | -7/+10 |
* | Merge of branches/full-expr-4: | xleroy | 2010-08-18 | 1 | -125/+131 |
* | Updated Caml parts to match new representation for global variables. | xleroy | 2010-05-26 | 1 | -10/+13 |
* | Add "fabs" (floating-point absolute value) as a unary operator in | xleroy | 2010-05-02 | 1 | -1/+2 |
* | Handling of builtins, continued. | xleroy | 2010-03-07 | 1 | -29/+28 |
* | Suppressed Init_pointer, now useless. Improved printing of strings in genera... | xleroy | 2010-03-03 | 1 | -4/+0 |
* | Support Clight initializers of the form "int * x = &y;". | xleroy | 2009-11-01 | 1 | -0/+5 |
* | Cil2Csyntax: added goto and labels; added assignment between structs | xleroy | 2009-08-16 | 1 | -0/+6 |
* | Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f... | xleroy | 2009-01-29 | 1 | -1/+0 |
* | Reorganized the development, modularizing away machine-dependent parts. | xleroy | 2008-12-30 | 1 | -0/+501 |