aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
Commit message (Collapse)AuthorAgeFilesLines
...
* 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-271-5/+5
| | | | | | | | | | | | 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-261-3/+6
| | | | | | | | | | | | | | | 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
|
* Improved handling and diagnostics for the `auto` storage class (#99)Xavier Leroy2018-04-251-24/+48
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* 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
* Check for redefinition of globals and preserve static initialized variables ↵Bernhard Schommer2018-04-091-3/+18
| | | | | | | | | | | | | | | | | (#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.
* 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-271-1/+5
| | | | | | | 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
* 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
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-2/+2
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Do not pass the env back from for stmt decls. (#42)Bernhard Schommer2017-12-121-7/+7
| | | | | | * Do not pass the env back from for stmt decls. This is the source of issue #211, the environment from the elaboration of the declaration and expressions in the for loop should not be passed back.
* Remove unused code. BUg 22642Bernhard Schommer2017-12-081-1/+0
|
* Store the different inlining cases.Bernhard Schommer2017-12-081-1/+1
| | | | | | | In order to correctly support the noinline attribute we must store whether the function was specified with an inline specifer, had a noinline attribute or nothing. Bug 22642
* Make redefinition of composite a fatal error.Bernhard Schommer2017-05-091-2/+1
| | | | | | | The redefinition of a composite with a different tag type is now a fatal error. This should avoid problems when the composite is used. Bug 21542
* Added check for large arrays.Bernhard Schommer2017-02-211-0/+1
| | | | | | | The check tests whether the size calculation of an array overflows or the array covers half of the available address space and reports an error in this case. Bug 21034
* Added gcc noinline attribute.Bernhard Schommer2017-02-191-0/+1
| | | | The noinline attribute prevents functions from inlining.
* Adopted unused variable and attribtue checkBernhard Schommer2017-02-171-0/+1
| | | | | | | | | The unused variable check now uses two passes. One to collect the used variables and one to report the unused variables. Futhermore attribute checks are extended to composite declaration. Also the check is now performed after elaboration. Bug 19872
* Added a simple check for unused variables.Bernhard Schommer2017-02-171-1/+3
| | | | | | | | | | | | | | | | | The check test whether the identifier is used at all in the function and if not issue a warning. It is not tested whether the usage is reachable at all, so int i; if (0) i; would not generate a warning. This is the same as gcc/clang does. The warning is disabled per default, but is active if -Wall is given. Bug 19872
* Do not optimize away the 'return 0' at end of 'main'Xavier Leroy2017-02-171-7/+5
| | | | | | As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through. Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'.
* Merge pull request #162 from AbsInt/return-analysis-2Xavier Leroy2017-02-151-6/+18
|\ | | | | | | Improved warnings related to function returns
| * More precise warnings about function returnsXavier Leroy2017-02-071-6/+18
| | | | | | | | | | | | | | | | | | | | | | | | This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.
* | Use Printf.sprintf instead of Format.sprintf when possibleXavier Leroy2017-02-091-4/+4
|/ | | | Minor performance tweak. Printf is more efficient for plain formats involving no boxes.
* Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-24/+46
|\
| * Preliminary support for the "noreturn" attributeXavier Leroy2017-02-061-11/+15
| | | | | | | | | | - Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type. - Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
| * Refactor the classification of attributesXavier Leroy2017-02-031-5/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce Cutil.class_of_attribute to return the class of the given attribute: one among Attr_type attribute related to types (e.g. "aligned") Attr_struct attribute related to struct/union/enum types (e.g. "packed") Attr_function attribute related to function types (e.g. "noreturn") Attr_name attribute related to variable and function declarations (e.g. "section") Attr_unknown attribute was not declared Cutil.declare_attribute is used to associate a class to a custom attribute. Standard attributes (const, volatile, _Alignas, etc) are Attr_type. cfronted/C2C.ml: declare the few attributes that CompCert honors currently. cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
| * Regression: type attributes and array modifiersXavier Leroy2017-02-011-2/+4
| | | | | | | | | | | | | | Owing to the peculiarities of array types in Cutil.change_attributes_type, type-related attributes of the array element type were duplicated on the array type. E.g. elaborating 'const int a[10][5]' produced "a is an array of 5 const arrays of 10 const ints" instead of "a is an array of 5 arrays of 10 const ints"
| * Revised elaboration of attributesXavier Leroy2017-01-311-13/+24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* | Remove all overriding opens in Elab.ml. Bug 19872Bernhard Schommer2017-02-031-2/+2
| |
* | Removed Cabshelper open and avoided shadowing.Bernhard Schommer2017-02-031-7/+6
| | | | | | | | | | | | | | | | The Cabshelper is only used in 4 places, so we don't need a global open. Furhtermore the String.t type is now inlined for Cabs to avoid shadowing problems in Elab.ml Bug 19872
* | Remove unused opens.Bernhard Schommer2017-02-031-32/+28
| | | | | | | | | | | | Format was only used in one place without explicit module prefix. The same holds for Env. Bug 19872
* | Removed no longer working check.Bernhard Schommer2017-02-031-14/+4
| | | | | | | | | | | | Since anonymous struct members are kept in the fieldlist, the fieldlist can never be empty in this case. Bug 19872
* | Avoid overflows and report an error.Bernhard Schommer2017-01-311-7/+7
| | | | | | | | | | | | | | Instead of multiplying the array constant directly with the size of the offset the cautious_mul function is used to detect potential overflows. Bug 20765
* | Normalize offset to size_t kind.Bernhard Schommer2017-01-311-2/+4
| |
* | Remove superfluous check.Bernhard Schommer2017-01-311-7/+4
| | | | | | | | | | | | Gcc and clang do not raise an error for this, also it should work for the last array element which can be without size. Bug 20765
* | New version to support designators.Bernhard Schommer2017-01-241-8/+33
| | | | | | | | | | | | | | | | | | The c standard allows member designators for offsetof. The current implementation works by recursively combining the offset of each of the member designators. For array access the size of the subtypes is multiplied by the index and for members the offset of the member is calculated. Bug 20765
* | Simplified version.Bernhard Schommer2017-01-201-10/+8
| | | | | | | | | | | | | | | | The problem was that sub structs are were not correctly aligned. The new version is much simpler and uses the sizeof_struct to calculate the individual offsets and add them up to get correct offest. Bug 20765
* | Also support union. Bug 20765Bernhard Schommer2017-01-201-3/+4
| |
* | Implement offsetof via builtin.Bernhard Schommer2017-01-201-0/+16
|/ | | | | | | | | | | | The implementation of offsetof as macro in the form ((size_t) &((ty*) NULL)->member) has the problem that it cannot be used everywhere were an integer constant expression is allowed, for example in initiliazers of global variables and there is also no check for the case that member is of bitifield type. The new implementation adds a builtin function for this which is replaced by an integer constant during elaboration. Bug 20765
generated by cgit (git 2.34.1) at 2024-07-01 15:52:03 +0000