summaryrefslogtreecommitdiff
path: root/cfrontend/Clight.v
Commit message (Expand)AuthorAge
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...Gravatar xleroy2011-07-16
* Merge of branch new-semantics: revised and strengthened top-level statements ...Gravatar xleroy2011-07-15
* Fix treatment of function pointers at function calls in the CompCert C and Cl...Gravatar xleroy2011-07-14
* Minor update in Clight (big-step)Gravatar blazy2011-06-08
* Ajout big-step Clight et preuve big-step -> small-stepGravatar blazy2011-05-25
* Nettoyages pour docGravatar xleroy2010-08-18
* Removed useless constraints on return type at Sreturn instructionsGravatar xleroy2010-08-18
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18