aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Initializersproof.v
Commit message (Expand)AuthorAgeFilesLines
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-155/+67
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-231-9/+7
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-5/+3
* Pointers one pastxleroy2013-02-151-3/+12
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-26/+42
* Make Clight independent of CompCert C.xleroy2012-10-081-0/+2
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-3/+45
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-4/+4
* Merge of the newmem branch:xleroy2012-05-211-2/+2
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+6
* Initializers: handle By_copy accesses (e.g. for &(glob.field))xleroy2012-02-071-1/+1
* Merge of the "volatile" branch:xleroy2012-02-041-41/+48
* Improved semantics of castsxleroy2011-07-171-9/+8
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-63/+40
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+3
* Incompatibility 8.3 / 8.3pl1xleroy2011-03-141-1/+1
* Slightly nicer semantics for initializationxleroy2011-03-131-28/+29
* More global initialization work done and proved in Coq.xleroy2011-03-131-12/+312
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-0/+555