aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
Commit message (Collapse)AuthorAgeFilesLines
* Reject incomplete types as return type.Bernhard Schommer2015-07-141-1/+4
|
* Use env1 instead of env to also have the type specifiers used in the return ↵Bernhard Schommer2015-07-091-1/+1
| | | | parameter.
* Propagated the composed type constructed build during identifier lookup.Bernhard Schommer2015-07-091-6/+6
|
* Add implicit "return 0;" at end of function "main".Xavier Leroy2015-07-081-1/+13
| | | | | | | | As per ISO C99, "hosted environment". "return 0" is added at the end of any function named "main" that has "int" as return type. If the name is "main" but the return type is not "int", emit a warning and do not add anything.
* Turn "redefinition with an incompatible type" warning into an error.Xavier Leroy2015-07-081-1/+6
| | | | Also: improve error message by showing old and new types.
* Simple fix for problem with local extern.Bernhard Schommer2015-06-241-0/+1
|
* Turn the error on anonymous structs/unions into a warning.Xavier Leroy2015-06-111-1/+1
| | | | | Otherwise we get too many errors on glibc's standard headers. A real error will occur when the anonymous struct/union is accessed.
* Error if, in the same scope, a typedef is redefined as a variable, or a ↵Xavier Leroy2015-06-061-2/+8
| | | | variable is redefined as a typedef.
* Make a register as storage specify to a fatal error.Bernhard Schommer2015-05-141-1/+1
|
* Changed the enter_or_refine_ident function to produce an error if a ↵Bernhard Schommer2015-05-131-6/+14
| | | | non-static declaration is followed by a static declaration/definition.
* Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) ↵Xavier Leroy2015-04-301-0/+14
| | | | and produce a diagnostic instead of ignoring them.
* Detect and reject "&" operator applied to "register" local variable or to a ↵Xavier Leroy2015-04-281-0/+17
| | | | bit field.
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-10/+25
|
* Issue #26: problems with big escape sequences in string/char literals.Xavier Leroy2015-03-071-7/+12
| | | | | | - Error instead of warning if escape sequence overflows one character. - Wrong normalization of L'x' to char instead of wchar_t. - More careful overflow tests.
* Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-8/+8
| | | | | | | | | | | | | Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* Wrong handling of block-local function declarations (again)Xavier Leroy2015-01-011-12/+7
| | | | | Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0 which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4
* Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-011-9/+11
| | | | | | | We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively. In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary. Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do. Net result is fewer warnings and type-checking that is closer to GCC/Clang.
* PR#12: regression introduced in commit 2d32afcXavier Leroy2014-12-301-2/+0
|
* PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-301-2/+2
| | | | | | | | | | - cparser/Machine indicates whether wchar_t is signed or not (it is signed int in Linux and BSD, but unsigned short in Win32) - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t" exists in the environment (e.g. after #include <stddef.h>). Only if wchar_t is not defined do we use the default from Machine. - Permit initialization of any integer array from a wide string literal, not just an array of wchar_t.
* PR#11: support sizeof(struct {...}) and _Alignof(struct {...})Xavier Leroy2014-12-301-25/+38
| | | | This is a partial fix because other cases of struct definitions within type-names are still not handled, e.g. (struct { ... } *) <expr>. However, error reporting was improved for these cases.
* Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-261-12/+7
|
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-388/+393
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 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
generated by cgit (git 2.34.1) at 2024-07-03 09:23:52 +0000