aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
Commit message (Collapse)AuthorAgeFilesLines
* bug 19234, inherit varargs flag from previous function definitions for KR ↵Michael Schmidt2016-06-281-4/+19
| | | | conversion
* Revised handling of old-style, K&R function definitionsXavier Leroy2016-06-241-63/+130
| | | | | | | | This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in float f (x) float x; { return x; } "x" is passed with type "double", and must be converted to "float" at the beginning of the function.
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-2/+5
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* Pass the updated env through elab_expr.Bernhard Schommer2016-06-211-149/+166
| | | | | | Since casts, sizeof, etc. expressions can introduce new types we also need to add these to the environment and pass it through. Bug 17814
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
* Revert initialization check, bug 18000Michael Schmidt2016-04-051-8/+0
|
* Match type size with size of wchar_t when initializing TInt arrays with wide ↵Michael Schmidt2016-04-051-1/+1
| | | | strings, bug 18000
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-2/+2
|
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-0/+8
|
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-13/+23
| | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-50/+50
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-101-3/+3
| | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Code cleanup.Bernhard Schommer2016-03-101-65/+63
| | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Make void always incomplete and exit on void members.Bernhard Schommer2016-02-021-1/+2
| | | | | | Since we cannot construct a default initializer for void types we need to exit earlier. Bug 18004.
* Do test for wrap around on singed ocaml integers.Bernhard Schommer2016-01-281-1/+1
| | | | | | In parse_int it was not tested if the value of v is smaller than zero. This allowed it that certain large integers were accepted due to wrap around.
* Issue #71: incorrect initialization of wchar_t arrays from wide string literalXavier Leroy2015-11-131-6/+6
| | | | Regression test added in regression/initializers.c
* Merge remote-tracking branch 'origin/master' into parser_fixJacques-Henri Jourdan2015-11-041-16/+16
|\
| * Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-24/+24
| |
* | Better handling of old-style K&R function declarations:Jacques-Henri Jourdan2015-11-011-92/+104
|/ | | | | | - Added a Cabs.PROTO_OLD constructor to Cabs.decl_type - Refactored the Parser.vy and pre_parser.mly grammars - Rewritten the conversion of old function definitions to new-style
* 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.