aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-293-4/+13
* driver: removed option -flonglongxleroy2013-04-224-25/+52
* Labeled statements inside switch were incorrectly processed.xleroy2013-04-221-0/+3
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-2019-1084/+1261
* Error when calling un-prototyped function.xleroy2013-03-251-6/+8
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-235-66/+76
* Fixed parsing of hex float literals 0xNNNpMMM.xleroy2013-03-111-1/+1
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-14/+8
* Constant propagation within __builtin_annot.xleroy2013-02-242-6/+9
* Pointers one pastxleroy2013-02-155-51/+82
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-103-41/+38
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-1/+5
* Camlcoq.ml: bug in conversion Z to stringv1.12.1xleroy2013-01-291-1/+1
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-2912-436/+454
* Avoid generating some obviously useless casts.xleroy2013-01-082-2/+36
* Put clighgen files in exportclight/xleroy2013-01-051-538/+0
* Print Swhile loops. Fix indentation.xleroy2013-01-051-8/+12
* Remove some useless "Require".xleroy2012-12-309-12/+0
* Merge of the clightgen branch:xleroy2012-12-2916-2562/+4341
* Support for inline assembly (asm statements).xleroy2012-12-182-2/+28
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-127-114/+106
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-2/+48
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-143-562/+693
* Make Clight independent of CompCert C.xleroy2012-10-0817-1364/+1493
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-0618-1935/+2036
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-4/+2
* Forgot to collect types of expressionsxleroy2012-07-282-2/+6
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-236-18/+19
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-2/+2
* Accept long double literals if -flongdouble is given.xleroy2012-07-101-1/+1
* Revert unintentional commit #1955xleroy2012-07-062-7/+6
* Ajout trunk CompCertblazy2012-07-042-6/+7
* More aggressive 'uncasting' before storing small integersxleroy2012-06-302-104/+145
* Use Flocq for floatsxleroy2012-06-283-5/+5
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-093-8/+14
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-2/+2
* Merge of the newmem branch:xleroy2012-05-213-150/+126
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-285-40/+11
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-091-0/+1
* Cprint: export Cprint.attributesxleroy2012-03-071-4/+16
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-1/+7
* Remove 'near-code' access mode, makes no sense in CompCertxleroy2012-03-061-2/+1
* Problems with multiple declarations of publically-visible identifiersxleroy2012-02-291-10/+33
* Better printing of pointer values and of locations.xleroy2012-02-291-10/+16
* Make CPragmas common to all ports.xleroy2012-02-271-0/+108
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-2615-14/+102
* Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr ifxleroy2012-02-254-98/+197
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-85/+44
* The C declaration associated with __stringlit_N globals now has type const ch...xleroy2012-02-201-1/+2
* Don't print external declarations for builtins.xleroy2012-02-182-4/+8