aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* Warn for volatile accesses to compositesxleroy2013-10-161-0/+8
* Merge of the "alignas" branch.xleroy2013-10-0511-137/+234
* Change the way arguments to __builtin_annot are converted. Use the same conv...xleroy2013-09-141-2/+6
* Revised handling of int->float conversions:xleroy2013-07-084-14/+25
* Bad printing of alignment on 'comm' symbols.xleroy2013-07-071-2/+6
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-035-14/+21
* Merge of the "princeton" branch:xleroy2013-06-169-244/+312
* Merge of the float32 branch: xleroy2013-05-192-1/+8
* Issue with simplification of nested ?: expressions of different types.xleroy2013-05-193-85/+129
* Preliminary support for debugging info (-g).xleroy2013-05-172-31/+58
* "->" can be applied to an array, not just a pointer.xleroy2013-05-161-1/+1
* Missing case: initialization of a global variable of type _Bool.xleroy2013-05-082-1/+2
* Revised semantics and compilation of 2-argument C operators to better match xleroy2013-05-063-194/+152
* 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