aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgen.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-44/+95
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-44/+95
* | Oexpect in frontendDavid Monniaux2020-04-071-0/+6
|/
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-4/+33
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-2/+2
* Use "Local" as prefixXavier Leroy2017-02-131-2/+2
* Regression: handling of integer + pointer in CompCert CXavier Leroy2016-10-061-18/+23
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-42/+66
* Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-29/+43
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-11/+11
* Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-301-1/+1
* Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-221-86/+93
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-1/+5
* Merge of "newspilling" branch:xleroy2014-07-231-36/+74
* Clean-up pass on C types:xleroy2014-04-231-6/+6
* __builtin_absfloat can be applied to integers too.xleroy2014-03-291-4/+12
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-7/+28
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-5/+4
* - Recognize __builtin_fabs as an operator, not just a builtin,xleroy2013-11-061-0/+1
* Merge of the "alignas" branch.xleroy2013-10-051-1/+1
* Revised handling of int->float conversions:xleroy2013-07-081-5/+7
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-5/+7
* Revised semantics and compilation of 2-argument C operators to better match xleroy2013-05-061-83/+67
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-0/+2
* driver: removed option -flonglongxleroy2013-04-221-0/+2
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-64/+142
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-5/+2
* Merge of the clightgen branch:xleroy2012-12-291-99/+17
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-2/+10
* Make Clight independent of CompCert C.xleroy2012-10-081-31/+32
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-124/+42
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-1/+1
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-2/+0
* Merge of the "volatile" branch:xleroy2012-02-041-28/+72
* Cleaned up old commented-out partsxleroy2011-08-191-26/+1
* Improved semantics of castsxleroy2011-07-171-1/+28
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-2/+4
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-2/+2
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+3
* Special case for while(1), for(..., 1, ...) and do ... while(0) loops.xleroy2011-03-151-5/+20
* Merge of branches/full-expr-4:xleroy2010-08-181-162/+134
* Support for inlined built-ins.xleroy2010-06-291-2/+2
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-0/+4
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-6/+1
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-021-2/+2
* No '\n' in Coq strings...xleroy2009-08-181-1/+1
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-29/+16
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-7/+3
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-4/+12
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12