aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
Commit message (Collapse)AuthorAgeFilesLines
* Improve error reporting for unsupported compound literals.xleroy2014-08-201-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2608 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improve error detection and error messages for enums.xleroy2014-08-171-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2568 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Spurious error on a local static function declarationxleroy2014-08-131-0/+1
| | | | | | | ("static int f(void);" inside a function). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2563 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In enter_or_refine_ident: revised handling of "extern" decls.xleroy2014-05-181-29/+38
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another corner case for string literal initializers: char * x[] = { "lit" }xleroy2014-05-181-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-151-1/+12
| | | | | | | | - Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-121-108/+44
| | | | | | | | | | - Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Incorrect conversion of K&R functions. Example of problem:xleroy2014-05-121-2/+3
| | | | | | | void * foo(s, u) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix string litteral parsingjjourdan2014-05-111-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2490 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed regression on initializers of the form T x[N] = "literal";xleroy2014-05-081-8/+10
| | | | | | | where T is a typedef for a character type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stern warning on non-prototype function definitions.xleroy2014-05-051-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2480 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for old-style K&R function definitions.xleroy2014-05-051-0/+46
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2478 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-306/+375
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean-up pass on C types:xleroy2014-04-231-12/+14
| | | | | | | | | | | | | - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-5/+2
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-281-129/+313
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-9/+15
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-011-4/+8
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Catch and report Env errors arising out of some Cutil functionsxleroy2013-12-301-7/+8
| | | | | | | (incomplete_type, sizeof, etc). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2393 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab.ml: more warnings.xleroy2013-12-301-4/+9
| | | | | | | Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved detection of variables with incomplete types.xleroy2013-12-301-4/+9
| | | | | | | Additional warnings for empty initializer braces and zero-sized arrays. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-2/+3
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revise parsing of character constants for conformance with ISO C 99.xleroy2013-10-251-12/+13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2352 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typing of integer literals: follow C99 rules exactly.xleroy2013-10-211-28/+29
| | | | | | | Comments: make reference to the C99 standard. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-1/+20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2339:xleroy2013-10-051-1/+1
| | | | | | | don't complain about parameter redefinition for unnamed parameters. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2340 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab:xleroy2013-10-041-22/+27
| | | | | | | | | | | - bad error recovery on bitfield with 'long long' type - check for redefinition of function parameters Bitfields: - when assigning to a bitfield, cast the RHS to "unsigned int" (it matters if the RHS is long long). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize attribute((packed)) after a "struct {...}" and not just between ↵xleroy2013-06-211-18/+31
| | | | | | "struct" and "{", for compatibility with GCC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support __attribute__(ident) where ident is not bound. Useful for GCC ↵xleroy2013-05-131-3/+6
| | | | | | compatibility in general and MacOS 10.8 standard includes in particular. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2248 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better locations for error messages relative to type specifiers.xleroy2013-03-251-14/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2159 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-32/+44
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-18/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-4/+4
| | | | | | | cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-19/+12
| | | | | | | | | | and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-041-2/+2
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Corrected initialization of char arrays by string literals.xleroy2011-10-171-24/+23
| | | | | | | Added -flongdouble option (to turn long double into double) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1731 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: don't generate "vfd" directive, useless?xleroy2011-08-221-7/+7
| | | | | | | cparser: distinguish more carefully between lvalues and modifiable lvalues. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1722 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong check: &e must be rejected if e has array type and is not a l-value.xleroy2011-08-211-8/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1720 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check for duplicate label definitionsxleroy2011-07-181-7/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1687 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More precise typechecking of statementsxleroy2011-07-171-33/+75
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1686 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵xleroy2011-06-131-11/+0
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Silence a warning that happens all too often in MacOS Xxleroy2011-05-121-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1654 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser: support for attributes over struct and union.xleroy2011-05-121-17/+22
| | | | | | | | cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-2/+0
| | | | | | | | | | Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support compile-time constant expressions as arguments to gcc-style attributesxleroy2011-04-201-23/+30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1641 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/Elab: __attribute, not attributexleroy2011-04-161-1/+1
| | | | | | | | ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of GCC attributes. Preliminary, untested support for ↵xleroy2011-04-141-16/+22
| | | | | | __aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of sizeof(string-literal)xleroy2011-03-151-5/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for IA32-Cygwin.xleroy2010-09-081-1/+1
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adding __builtin_annotationxleroy2010-09-011-0/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-03 10:09:37 +0000