aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | Better error message for function initializerBernhard Schommer2016-08-221-0/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initializers for function variables are not allowed. CompCert now reports an error and exits. Bug 19606
| * | | | Test for incomplete type during initialization.Bernhard Schommer2016-08-221-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before the initializazion is computed we check wether the type is incomplete. Bug 19601
| * | | | Error for va_start in non-vararg function.Bernhard Schommer2016-08-221-27/+31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert now reports an error for usage of the va_start macro in non variadic functions. Bug 19600.
| * | | | Added check for incomplete parameter types.Bernhard Schommer2016-08-201-1/+5
| | | | | | | | | | | | | | | | | | | | | | | | | Parameters also need to be checked for incomplete types. Bug 19596
| * | | | Exit earlier on invalid alignof and sizeof.Bernhard Schommer2016-08-191-4/+4
| | |_|/ | |/| | | | | | | | | | | | | | | | | | Alginof and sizeof applied to incomplete types now exit earlier with a fatal error. Bug 19594.
| * | | Disallow void as type for variables.Bernhard Schommer2016-08-181-0/+2
| | |/ | |/| | | | | | | | | | | | | This allows problems in elaboration of the initializers for variables of void type. Bug 19577.
| * | Exit earlier on empty union.Bernhard Schommer2016-08-171-1/+5
| | | | | | | | | | | | | | | | | | | | | Instead of a warning for an empty union CompCert reports an error and exits. This avoids problems during the generation of initializers for these. Bug 19565.
| * | Catch attribute excpetion in _Alignas elabBernhard Schommer2016-08-171-0/+1
| | | | | | | | | | | | | | | | | | The exception Wrong_attr_arg raised is now catched during the translation of the wrong _Alignas attributes. Bug 19568.
| * | Fixed typo. Bug 19504Bernhard Schommer2016-08-081-1/+1
| | |
| * | Added error check before transformations.Bernhard Schommer2016-08-084-3/+7
| | | | | | | | | | | | | | | | | | Added a check for errors after the elab phases to avoid problems in the transformations due to broken input programs. Bug 19504
| * | Exit earlier on wrong return types.Bernhard Schommer2016-08-071-1/+1
| |/ | | | | | | | | | | Return with a expression that is not compatible with the given return type of a function now causes and fatal error, to avoid problems with later transformation passes depending on it.
* | Added raw printing of types without formatting.Bernhard Schommer2016-08-163-5/+11
| | | | | | | | | | | | This avoids introducing line breaks during printing of function types. Bug 18004
* | Additional test for color output.Bernhard Schommer2016-08-052-39/+59
| | | | | | | | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
* | Classified all warnings and added various options.Bernhard Schommer2016-07-2913-319/+650
|/ | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* Nicer error message for redefinitions with incompatible typeXavier Leroy2016-07-221-3/+4
|
* Improved handling of C90 calls to undeclared functionsXavier Leroy2016-07-211-73/+75
| | | | | | In a call such as "f(expr, ..., expr)", if the identifier "f" is not declared, declare it as specified in the ISO C90 standard, namely like "extern int f()" would do it. Previously, the declaration was done "on the side" and not properly recorded in the environments. The diff is relatively large because the "enter_or_refine_ident" had to be moved up in the file.
* Revised handling of block-scoped extern declarationsXavier Leroy2016-07-211-46/+93
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, CompCert incorrectly handles 'extern' and function declarations within a block. For example: int main(void) { { extern int i; i = 0; } { extern float i; i = 10; } } CompCert fails to detect the inconsistent declarations of "i" in the two blocks, simply because the first declaration is not in scope when the second declaration is processed. This commit changes the elaboration of file-scope declarations, block-scope "extern" declarations and block-scope function declarations so that they are checked against possible earlier declarations found in the already-elaborated top-level declarations, instead of in the current typing environment. Owing to the lifting of block-scoped extern and static declarations to the top-level already performed by the elaboration pass, the already-elaborated top-level declarations give an accurate view of the declarations of variables with internal or external linkage already encountered and processed, even if they are not currently in scope.
* Port to Coq 8.5pl2Xavier Leroy2016-07-088-81/+106
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* 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-212-6/+8
| | | | | | | | 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
* Fixed a comment.François Pottier2016-05-272-5/+3
|
* 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
|
* Merge pull request #95 from AbsInt/noreturnBernhard Schommer2016-04-048-25/+68
|\ | | | | Added the _Noreturn keyword.
| * Added the _Noreturn keyword.Bernhard Schommer2016-03-238-25/+68
| | | | | | | | | | | | | | | | 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
* | Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-312-3/+3
|/
* Fix a bug in the pre-parser.Jacques-Henri Jourdan2016-03-231-0/+1
|
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1514-139/+139
| | | | | | 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-1016-230/+194
| | | | | | 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.
* Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| | | | | | Compare the underlying array types, otherwise we end up in a endless recursion. Bug 18374
* Make void always incomplete and exit on void members.Bernhard Schommer2016-02-022-2/+8
| | | | | | 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.
* Allow adding of attributes in valid_assignment_attr.Bernhard Schommer2016-01-281-2/+2
| | | | | Implementing the same behavior as gcc anc clang. Bug 18004
* Enum is compatible to its integer type.Bernhard Schommer2015-12-171-0/+3
| | | | | | The C standard specifies that an enum type should be compatible to some integer type (ISO/IEC 9899:TC3 §6.7.2.2p4). Fix 16692
* More gcc/newlib compatibility code.Bernhard Schommer2015-12-111-1/+8
| | | | | | | | | | Some newlib headers use the __extension__ keyword which suppresses warnings for gcc extensions in strict mode. CompCert now ignores this keyword for the gnu backends. Also it seems that stddef of the gcc defines wint_t even though it should not. However some libs rely on this. So wint_t is now defined in CompCert's stddef header. Bug 17613.
* Revise and simplify the -fstruct-return and -fstruct-passing options.Xavier Leroy2015-12-081-2/+2
| | | | | | - Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing' - Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful. - Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
* Fixed regression introduce by merge of PR#69.Bernhard Schommer2015-12-031-4/+1
| | | | | | | Since the identifier of a function definition and of its declaration are equal we only should remove functions if the function iteself is removed. Bug 17724.
* Open files in binary mode.Bernhard Schommer2015-11-301-1/+1
| | | | | | On windows opening files in text mode can result in errors due to non-windows compatible input. Thus open files only in binary mode. Bug 17664
* For uniformity with other messages, added an "Ill-formed expression.".François Pottier2015-11-241-0/+1
|
* Use 1-based column numbers instead of 0-based.François Pottier2015-11-241-2/+2
| | | | This seems to agree with clang and with the emacs C mode.
* Update of the auto-generated comments.François Pottier2015-11-241-610/+611
|
* A simplification in the grammar, leading to fewer states in the automatonFrançois Pottier2015-11-242-19/+4
| | | | and merging two error states into one. There should be no observable change.
* Fix a typo in a syntax error message.François Pottier2015-11-231-1/+1
|