aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/ClightBigstep.v
Commit message (Expand)AuthorAgeFilesLines
* Native support for bit fields (#400)Xavier Leroy2021-08-221-3/+3
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-021-4/+4
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-31/+31
* Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-291-2/+2
* 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