aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-2/+7
* driver: removed option -flonglongxleroy2013-04-221-0/+12
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-277/+249
* Pointers one pastxleroy2013-02-151-1/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+5
* Merge of the clightgen branch:xleroy2012-12-291-310/+76
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-29/+8
* Make Clight independent of CompCert C.xleroy2012-10-081-11/+11
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-431/+146
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-4/+2
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-8/+6
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-2/+0
* Merge of the "volatile" branch:xleroy2012-02-041-175/+344
* Merge of the nonstrict-ops branch:xleroy2012-01-141-9/+11
* Cleaned up old commented-out partsxleroy2011-08-191-12/+0
* Improved semantics of castsxleroy2011-07-171-55/+53
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-110/+73
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-42/+9
* Fix treatment of function pointers at function calls in the CompCert C and Cl...xleroy2011-07-141-2/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-5/+7
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.xleroy2011-03-151-17/+49
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+13
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-2/+4
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+1869