aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
Commit message (Collapse)AuthorAgeFilesLines
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-24/+24
|
* Handle the special case of a typedef to void funciton parameter to beBernhard Schommer2015-10-051-2/+2
| | | | handled as a function with void parameter.
* Allow redefinition of a typedef with the same name.Bernhard Schommer2015-10-041-7/+15
| | | | | C11 allows a typedef redefinition if the types are the same. We now allow this also and issue a warning and an error if the types are different.
* Merge pull request #57 from jhjourdan/parser_fixBernhard Schommer2015-10-011-17/+0
|\ | | | | Correction of a few bugs in the pre-parser, added comments.
| * Fixed a few bugs in the pre parser. In particular, the following codeJacques-Henri Jourdan2015-09-301-17/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | was not parsed correctly: typedef int a; int f() { for(int a; ;) if(1); a * x; } Additionnaly, I tried to add some comments in the pre-parser code, especially for the different hacks used to solve various conflicts.
* | Record the scope structure during unblocking.Bernhard Schommer2015-09-221-1/+1
| | | | | | | | | | | | Instead of creating separate annotations for the local variables we call the Debug.add_lvar_scope and we construct a mapping from function id + scope id to scope information.
* | Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-211-1/+1
|\| | | | | | | | | | | Conflicts: debug/CtoDwarf.ml debug/DwarfPrinter.ml
| * Global register variables result in fatal error.Bernhard Schommer2015-09-081-1/+1
| | | | | | | | | | If they only report an error an assertion failure in Reame.ml was triggered.
* | New version of adding scopes etc.Bernhard Schommer2015-09-201-1/+1
| | | | | | | | | | Instead of reimplementing the whole scope handling in the debug information use the existing functionality and fill the scopes explicitly in the functions.
* | Started implementing the scope for the Debug Informations.Bernhard Schommer2015-09-181-1/+3
| | | | | | | | | | | | Scopes will be handled by a stack of all open scopes. This stack then can also be used to generate the debug directives to track the scopes through the rest of the passes.
* | First version with computation of dwarf info from debug info.Bernhard Schommer2015-09-171-3/+3
| | | | | | | | | | Introduced a new dwarf generation from the information collected in the DebugInformation and removed the old CtODwarf translation.
* | Move more functionality in the new interface.Bernhard Schommer2015-09-161-13/+15
|/ | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* 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