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