aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintCsyntax.ml
Commit message (Expand)AuthorAgeFilesLines
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+10
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-231-15/+13
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-1/+1
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-13/+14
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+2
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-1/+22
* Forgot to collect types of expressionsxleroy2012-07-281-1/+3
* Use Flocq for floatsxleroy2012-06-281-3/+3
* Better printing of pointer values and of locations.xleroy2012-02-291-10/+16
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-1/+5
* Don't print external declarations for builtins.xleroy2012-02-181-2/+4
* Merge of the "volatile" branch:xleroy2012-02-041-23/+32
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-8/+8
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-7/+10
* Merge of branches/full-expr-4:xleroy2010-08-181-125/+131
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-10/+13
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-1/+2
* Handling of builtins, continued.xleroy2010-03-071-29/+28
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-4/+0
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+5
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-0/+6
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-291-1/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+501