aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/ClightBigstep.v
Commit message (Expand)AuthorAgeFilesLines
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-9/+9
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-5/+7
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-10/+10
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-9/+9
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-0/+583