aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Csyntax.v
Commit message (Expand)AuthorAgeFilesLines
* Native support for bit fields (#400)Xavier Leroy2021-08-221-2/+2
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+12
* Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-1/+1
* Define linking for Csyntax and Clight programs.Xavier Leroy2016-03-061-52/+10
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-5/+5
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-211-18/+22
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-4/+41
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-131-3/+4
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-1/+1
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-3/+4
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-3/+3
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Make Clight independent of CompCert C.xleroy2012-10-081-782/+7
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-23/+13
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+2
* Merge of the "volatile" branch:xleroy2012-02-041-187/+211
* Improved semantics of castsxleroy2011-07-171-1/+22
* Merge of branch "unsigned-offsets":xleroy2011-04-091-8/+8
* Adding __builtin_annotationxleroy2010-09-011-0/+67
* Merge of branches/full-expr-4:xleroy2010-08-181-132/+375
* Support for inlined built-ins.xleroy2010-06-291-5/+1
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-1/+2
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-021-19/+22
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-1/+8
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-26/+26
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-1/+91
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-0/+3
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-131-10/+8
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-7/+2
* Documentationxleroy2007-08-051-107/+192
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-4/+7
* Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...xleroy2006-09-111-8/+12
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-16/+1
* Fusion de la branche "traces":xleroy2006-09-041-0/+456