aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Expand)AuthorAgeFilesLines
* 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
* Initializers: handle By_copy accesses (e.g. for &(glob.field))xleroy2012-02-073-47/+8
* Merge of the "volatile" branch:xleroy2012-02-0419-2045/+3297
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-19/+71
* Merge of the nonstrict-ops branch:xleroy2012-01-143-284/+828
* More careful updating of current location for error msgs.xleroy2011-11-261-6/+10
* Fixed serious bug in handling of volatile arrays.xleroy2011-11-261-2/+5
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-183-31/+26
* Corrected initialization of char arrays by string literals.xleroy2011-10-171-1/+3
* MAJ licencexleroy2011-08-231-0/+3
* arm/PrintAsm: don't generate "vfd" directive, useless?xleroy2011-08-221-1/+1
* Cleaned up old commented-out partsxleroy2011-08-196-194/+1
* Presimplification SimplVolatile: cleaned up and integrated.xleroy2011-08-182-1/+2
* Flag long long and long double literalsxleroy2011-07-311-2/+6
* Interp.ml: initialize PRNGxleroy2011-07-291-2/+14