aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* 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