aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Clight.v
Commit message (Expand)AuthorAgeFilesLines
* Merge of the clightgen branch:xleroy2012-12-291-11/+56
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-554/+0
* Make Clight independent of CompCert C.xleroy2012-10-081-18/+43
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-471/+291
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-4/+5
* Merge of the "volatile" branch:xleroy2012-02-041-26/+51
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-77/+47
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-31/+35
* Fix treatment of function pointers at function calls in the CompCert C and Cl...xleroy2011-07-141-10/+10
* Minor update in Clight (big-step)blazy2011-06-081-18/+18
* Ajout big-step Clight et preuve big-step -> small-stepblazy2011-05-251-1/+769
* Nettoyages pour docxleroy2010-08-181-12/+6
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-1/+0
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+623