aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Fix menhirLib namespaces, following changes in Menhir version 20180530Jacques-Henri Jourdan2018-06-0611-0/+0
|
* Warn for defs and uses of static variables in nonstatic inline functionsXavier Leroy2018-06-043-16/+42
| | | | | | | Nonstatic inline functions can be expanded in several compilation units. The static variables in question may differ between different expansions. This is a manual merge and adaptation of pull request #P95 by @bschommer.
* Parameterize elab_expr by the full elaboration contextXavier Leroy2018-06-041-30/+42
| | | | | | | | | | | | Before, we would pass just the `ctx_vararg` component of the context to `elab_expr` as a Boolean argument. For future extensions, we will need to pass more of the context to `elab_expr`, so why not pass the whole context? This is what this commit does. The `stmt_context` type is renamed `elab_context` and its definition is moved earlier. The `ctx` argument is passed as is from `elab_stmt` to `elab_expr`.
* Support redefinition of a typedef in another scope (#122)Xavier Leroy2018-06-041-2/+2
| | | | | | | The current check for redefinition is too strict, ruling out e.g. ``` typedef int t; void f(void) { typedef char t; } ```
* Turn off the warning "C11 extension" by defaultXavier Leroy2018-06-041-1/+0
| | | | | | These are extensions w.r.t. C99, not incompatible changes. Nothing bad can happen if those C11 features are used, except making the code incompatible with C99.
* Warn that _Alignas and _Alignof are C11 extensionsXavier Leroy2018-06-041-1/+3
| | | | Consistently with _Noreturn, anonymous structs, etc.
* Allow align attribute of zero. (#120)Bernhard Schommer2018-05-291-2/+2
| | | | | | As the standard says (and is already implemented) an _Alignas(0) does not change the alignment at all. The same holds for the gcc attribute. Bug 23387
* Removed duplicated whitespace. Bug 23660Bernhard Schommer2018-05-291-1/+1
|
* String literals are l-values and have array types (#116)Bernhard Schommer2018-05-273-17/+14
| | | | | | | | | | | | | | | | | * Allow strings literals as lvalues. Strings and WStrings literals are lvalues, thus it is allowed to take their addresses. Bug 23356. * String literals have types "array of (wide) char", not "pointer to (wide) char" The pointer types were a leftover from the early, CIL-based C frontend. * Remove special case for sizeof("string literal") during elaboration No longer needed now that literals have array types.
* Preserve storage class for functions declared within a blockXavier Leroy2018-05-261-7/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to the introduction of the Storage_auto storage class in commit 760e422. For functions declared within a block, we used to set their storage class to "extern": { { int f(void); ---> extern int f(void); } } This helped enter_or_refine_ident understand that those declarations have linkage. Now that we have Storage_auto, this commit teaches enter_or_refine_ident that local declarations have no linkage if auto or static, and have linkage if extern or default. Then, there is no need to change storage class to extern for locally-declared functions. In turn, this improves the "extern-after-definition" warning recently introduced, avoiding a bizarre warning in the following case: int foo(void){return 0;} int main(void){ int foo(void); return foo(); }
* Warning for extern declaration after definition.Bernhard Schommer2018-05-263-1/+11
| | | | | | | | | Warning for change of storage class after the definition of a function from default storage class to extern storage class. This only plays a role if the function is also declared inline, since for inline functions with default storage class no code is generated, but for inline functions with extern storage class code should be generated. Bug 23512
* Reject "e1, e2" as a compile-time constant expressionXavier Leroy2018-05-241-5/+5
| | | | This is what ISO C99 says, even though C++ and some C compilers accept it.
* Harden attributes_of_types against out-of-scope structs/unions/enumsXavier Leroy2018-05-071-3/+12
| | | | | | | | | | | | | | | | | | | | | | | | In rare cases we can end up querying the attributes of a struct, union or enum type that is no longer in scope and therefore not bound in the current environment. Instead of raising an Env.Error_ exception in this case, this commit treats such structs / unions / enums as having no attributes attached to their definitions: only the attributes carried by the type expression are returned. One example where this occurs is the following, made possible by the previous commit ("Revised elaboration of function definitions"): int f(struct s { int a; } * p) { return p-> a; } int g(void) { return f(NULL); } "struct s" is scoped within the definition of f. When we get to checking the call to f from g, checking that the NULL argument is compatible with the "struct s *" parameters, we're outside the scope of "struct s" and its definition is not found in the current environment.
* Revised elaboration of function definitions, part 2Xavier Leroy2018-05-071-65/+143
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Change elab_type_declarator and elab_fundef_name so that the latter returns two environments: the first one takes into account struct/union definitions from the function return type, while the second one also contains bindings for function parameters and struct/union definitions from the function parameter list. To this end the "kr_ok" bool argument of elab_type_declarator is repurposed and renamed "fundef". It controls not just whether K&R function declarators are supported, but also which bindings the returned environment contains. Change elab_fundef to adapt to the changes in elab_fundef_name and to maintain two environments: - the global environment, enriched with struct/union definitions from the function return type, and with the function binding itself; - the local environment, used for elaborating the body of the function, which also contains bindings for function parameters and struct/union definitions from the function parameter list. Change elab_funbody so that it does not open a new scope for elaborating the body, even though the body is represented as a block in the AST. The standard says that the function body is processed in the same scope where function parameters are declared, so that the following is illegal: int f(int x) { double x; ... } Introduce a variant enter_or_refine_function of enter_or_refine_ident where the fresh identifier to use (if no earlier declaration is found) is created in advance in an earlier scope. This helps implement the proper scoping of function names.
* Revised elaboration of function definitions, part 1Xavier Leroy2018-05-071-36/+40
| | | | | | | | | | | | | | | | Partial revert of commit ec95665e087d39e29ece455b90e7d5918dc88cee. That commit introduced a "keep_ty" parameter to type elaboration functions telling them to keep struct/union definitions occurring in function parameter lists and lift them to the outer environment. By setting keep_ty to true, the following could typecheck: int f(struct s { int a; } x) { return x.a; } However, "struct s" would escape the scope of the function definition and leak to the top-level environment, which is not correct. In subsequent commits we'll address the issues above differently, in a way that does not need the "keep_ty = true" behavior.
* Added a diagnostic for attributes dec after defBernhard Schommer2018-05-073-3/+19
| | | | | | The new warning is raise for function declaration after a function definition that introduce new attributes, which are ignored. Bug 23385
* Warning for comparison of incomplete pointers.Bernhard Schommer2018-05-071-0/+4
| | | | | | The C standards says that either both types must be pointer to complete compatible or incomplete compatible types. Bug 23631
* Check that variables declared in 'for' loops are local variables (#104)Bernhard Schommer2018-05-041-11/+11
| | | | | | | | | | | | | | * Check for static and extern variables in for The declaration inside of a for statement is not allowed to have static or extern storage duration. Bug 23330 * Also check that the declared variables don't have function types. * Also checks that no typedefs occur in 'for' declarations. * Simplify the `elab_declarations` function. It's used only to elaborate the whole program, and the resulting declarations and environment are ignored. So, replace `elab_declarations` by a simpler iteration over the program in `elab_program`.
* Reject empty declarations in K&R functions. (#107)Bernhard Schommer2018-05-041-0/+2
| | | | | Empty declarations in K&R function parameters are not allowed by the C standard. Bug 23375
* Reject arrays of incomplete type (#90)Bernhard Schommer2018-05-021-0/+2
| | | | The type of array elements must be complete. Bug 23341
* Also check statement of label statement.Bernhard Schommer2018-04-271-1/+2
|
* Detect duplicate 'case' or 'default' statements within a 'switch'Xavier Leroy2018-04-271-0/+41
| | | | Report an error in this case.
* Record value of constant expression in C.Scase constructorXavier Leroy2018-04-275-9/+9
| | | | | | | | | | | | The Elab pass checks that the argument of 'case' is a compile-time constant expression. This commit records the value of this expression in the C.Scase AST generated by Elab, so that it can be used for further diagnostics, i.e. checking (in Elab) for duplicate cases. Note that C2C ignores the recorded value and recomputes the value of the expression using Ceval.integer_expr. This is intentional: Ceval.integer_expr is more trustworthy, as it is formally verified against the CompCert C semantics.
* Detect 'case' and 'default' outside a 'switch' statementXavier Leroy2018-04-271-1/+7
| | | | Report an error in this case.
* Additional checks on typedefs (#101)Bernhard Schommer2018-04-261-0/+4
| | | | Typedefs should have a name and also should not contain _Noreturn. Bug 23381
* Earlier, more comprehensive check for constant initializers (#88)Xavier Leroy2018-04-263-4/+99
| | | | | | | | | | | | | | | This commit checks *during elaboration* that initializers for global variables or local static variables are compile-time constants. Before this commit, some non-constant initializers were detected later in the C2C pass, but others were eliminated by the Cleanup pass before being checked, and yet others could cause the Rename pass to abort. To determine which variables are constant l-values, we leverage the recent addition of the Storage_auto storage class and base the determination on the storage class of the identifier: 'auto' or 'register' is not constant, the others are constant.
* Check for enums that have the same tag as composites (#100)Bernhard Schommer2018-04-251-1/+8
| | | | | Enum tags, struct tags and union tags share a common namespace, thus having an enum with the same tag as a struct or union is not allowed. Bug 23548
* Add diagnostic for illegal use of void (Bug 23342)Michael Schmidt2018-04-251-0/+2
|
* Initialization of anonymous bit-fields in structsXavier Leroy2018-04-251-1/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | For anonymous bit-fields in structs, carrier fields may be introduced which are not initialized since no default initializer are generated earlier. This cause the translation in C2C to throw an error since too few initializers are available. Example: struct s2 { int : 10; int a; int : 10; char b; int : 10; short c; int : 10; } s2 = { 42, 'a', 43 }; To work around this issue we need to generate a default inializer for every new member that does not have a translated member. Based on P#80, with more efficient algorithms. Bug 23362
* Bitfields transformation: record the fields after transformationXavier Leroy2018-04-251-4/+20
| | | | | | | | | | | | | | For each struct or union that contains bitfields, we record the list of members after transformation, where bit fields were replaced by carrier fields. Right now we do not use this information but it will come handy to fix a problem with struct initialization. Also: clear the global hash tables on entry so that multiple runs of the Bitfields transformation don't interfere with each other. There probably was no interference before because identifiers are unique enough, but this is fragile.
* Initialization of union bit fieldsXavier Leroy2018-04-251-3/+12
| | | | | | | | | | | Bit fields in unions were initialized like normal fields, causing mismatch on the name of the field. Also: added function Bitfields.carrier_field and refactored. Patch by Bernhard Schommer. Bug 23362
* Improved handling and diagnostics for the `auto` storage class (#99)Xavier Leroy2018-04-254-26/+52
| | | | | | | | | | | | | | | | | | | | | | | | Previously, CompCert would just ignore the `auto` keyword, thus accepting incorrect top-level definitions such as ``` auto int x; auto void f(auto int x) { } ``` This commit introduces `auto` as a proper storage class (Storage_auto constructor in the C AST). It adds diagnostics for misuses of `auto`, often patterned after the existing diagnostics for misuses of `register`. Some error messages were corrected ("storage-class" -> "storage class") or made closer to those of clang. Finally, in the generated C AST and in C typing environments, block-scoped variables without an explicit storage class are recorded as Storage_auto instead of Storage_default. This is semantically correct (block-scoped variables default to `auto` behavior) and will help us distinguishing block-scoped variables from file-scoped variables in later developments.
* Use "fix <name> <number>" instead of "fix <number>"Xavier Leroy2018-04-251-8/+8
| | | | The "fix <number>" tactic is deprecated in Coq 8.8.0 and triggers warnings.
* Accept empty enum declaration after nonempty enum definition (#87)Bernhard Schommer2018-04-221-1/+1
| | | | Forward declarations of enums are not allowed in C99, however it is possible to have an empty enum declaration after the enum was defined.
* Better check for incomplete types in pointer subtraction (#92)Bernhard Schommer2018-04-201-0/+1
| | | | | | In the case of pointer subtraction both side can be pointers, for example if the difference between two array cells is calculated, so we need to check that both sides have complete types. Bug 23312
* Function defintions: keep the attributes from previous declarations (#89)Bernhard Schommer2018-04-191-1/+3
| | | | | | | | | | | | After calling enter_or_refine for a function identifier we need to keep the combined attributes. Here is an example where it makes a difference: ``` _Noreturn void f(int x); void f(int x) { } ``` Before this commit, the `_Noreturn` on the declaration is ignored when checking the definition. Bug 23385
* Revert "preserve static initialized variables (#81)"Xavier Leroy2018-04-101-9/+2
| | | | | | This part of PR#81 causes problems with long double static variables in math.h. Revert to the old behavior of not including static variables unless actually referenced.
* Check for redefinition of globals and preserve static initialized variables ↵Bernhard Schommer2018-04-092-6/+33
| | | | | | | | | | | | | | | | | (#81) * Added check for redefinition of globals. Since Cleanup may remove duplicated static functions or global definitions we need to check for duplication during elaboration, not just in C2C. Bug 23410 * Do not eliminate unreferenced static variables with initializers This way all initialized variables make it to the C2C pass, where the initializers are checked for constant-ness. Bug 23410
* Reject illegal initializations of aggregates at top-level (#79)Xavier Leroy2018-04-061-1/+10
| | | | | | | Examples such as the following were accepted but are invalid ISO C: char c[4] = 42; struct S { int x, y; } = 42; This commit rejects such initializations at top-level. Bug 23372
* Allow declaration of composites in bitfield size.Bernhard Schommer2018-04-051-11/+20
| | | | | | It is allowed to define a composite within a bitfield size expression using for example sizeof. Bug 23360
* Error for subtraction arithmetic type - pointer type (#73)Bernhard Schommer2018-04-051-3/+0
| | | | | | Substraction is only allowed for pointer - pointer, pointer - arithmetic or arithmetic - arithmetic. This also leads to a retyping error later. Bug 23357
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-301-37/+56
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Consider: struct P { int x, y; } struct S { struct P p; } struct P p0 = { 1,2 }; struct S s1 = { .p = p0; .p.x = 3 }; ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e. the initialization of s1.p.y to p0.y implied by ".p = p0" is kept, even though the initialization of s1.p.x to p0.x is overwritten by ".p.x = 3". GCC, old versions of Clang, and previous versions of CompCert initialize s1.p.y to the default value 0. I.e. the initialization ".p = p0" is forgotten, leaving default values for the fields of .p before ".p.x = 3" takes effect. Implementing the proper ISO C99 semantics in CompCert is difficult, owing to a mismatch between the intended semantics and the C.init representation of initializers. This commit turns the delicate case of reinitialization above (re-initializing a member of a composite that has already been initialized as a whole) into a compile-time error. We will then see if the delicate case occurs in practice and needs further attention.
* Reject casts to struct/union types (#68)Bernhard Schommer2018-03-291-3/+0
| | | | | | | | | | | The ISO C99 standard allows cast only if the type name involved is either a void type or a scalar type. For compatibility with GCC and Clang we used to support casting a struct or union to exactly the same struct or union type. That does not seem useful in practice and complicates conformance testing. This commit gets rid of this exception to the C99 rule. Bug 23310
* Don't overwrite initializer of anonymous union member. (#69)Bernhard Schommer2018-03-291-1/+1
| | | | | Instead of overwriting the initializer of the anonymous member we should just keep it. Bug 23353
* Sizeof and _Alignof are not allowed on bit-fields (#67)Bernhard Schommer2018-03-273-1/+17
| | | | | | | Sizeof and _Alignof are not allowed on bit-fields Sizeof and _Alignof are not allowed to be applied to a expression that designates a bit-field member. Bug 23311
* Fix mistake in Bitfield transformation (#66)Michael Schmidt2018-03-271-2/+2
| | | Unions containing multiple bit fields were transformed incorrectly.
* Arrays should decay to pointers (#65)Bernhard Schommer2018-03-271-2/+3
| | | | | | | Arrays should decay to pointers except if they are used as operands of sizeof, _Alignof or as operand of the unary &. The "comma" sequencing operator was missing a "decay" on the type of its second argument. All other operators "decay" their operands correctly. Bug 23299 Bug 23311
* Improve error messages for anonymous bit-fields (#64)Bernhard Schommer2018-03-231-7/+10
| | | | | | If an anonymous bit-field member is declared wrong, i.e. a wrong type is used or a too large size is used the error message now prints <anonymous> instead of an empty string. Bug 23292
* Do not allow inline on main and warn for Noreturn (#63)Bernhard Schommer2018-03-231-0/+4
| | | | | | | | | | | | | | * Do not allow inline on main(). The C99 standard says that in a hosted environment inline shall not appear in a declaration of main. Bug 23274 * Added warning for _Noreturn on main(). The C11 standard does not allow any function specifier on the main function. Bug 23274
* StructPassing and annotations, continuedXavier Leroy2018-03-091-9/+7
| | | | | struct/union arguments to annotations should not be transformed at top level, but the regular function calls contained within must be transformed recursively.