summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof.v
Commit message (Expand)AuthorAge
* Merge of branch "unsigned-offsets":Gravatar xleroy2011-04-09
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.Gravatar xleroy2011-03-15
* Float.intoffloat and Float.intuoffloat are now partial functions.Gravatar xleroy2010-10-28
* Removed useless constraints on return type at Sreturn instructionsGravatar xleroy2010-08-18
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18