aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Check ptr arithmetic for ++ and --Bernhard Schommer2020-09-201-10/+16
| | | | | Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
* Add new static-assert token for deLexer utility; bug 29273Michael Schmidt2020-08-041-0/+1
|
* Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
|
* Allow string_literals_list in _Static_assert.Bernhard Schommer2020-07-272-24/+25
| | | | | | Not all pre-processors concatenate string literal lists, however they are allowed in _Static_assert. This is similar to the rules for inline assembly etc.
* More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
| | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments.
* cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
|
* Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
* Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
|
* Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
* Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
|
* Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
| | | | | | We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment.
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-5/+5
|
* Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Use library function.Bernhard Schommer2020-06-281-4/+1
| | | | | | | The function String.uppercase was deprecated and the replacement function String.upercase_ascii was only available from OCaml 4.03.0. Since the minimal OCaml version is now 4.05.0 we can use the function String.upercase_ascii.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-2/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
|
* Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
|
* Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
|
* Include typedef name in error message (#228)Bernhard Schommer2020-03-041-2/+2
| | | In case of redefinition of a typedef name with a different type.
* The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
| | | | See ISO C2011 standard, section 6.4.4.4 para 11.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
* Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
| | | | Some preprocessors don't remove the vertical tab from the input so we should be able to handle them in the lexer.
* Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
* Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
|
* Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
| | | | | | | Instead of constructing four different lists for maintaining the state of the warnings only one list is now used. This list contains the name of the warning and a boolean indicating whether this option should be active by default. The rest is computed from this list.
* Remove duplicated ticks.Bernhard Schommer2019-10-011-2/+2
|
* Use pointer type for evaluated constants.Bernhard Schommer2019-10-011-1/+1
|
* Various improvements for diagnostics.Bernhard Schommer2019-09-303-10/+34
| | | | | | | | | | | | | | | | | | | | | | | | * Extend check for incomplete type. Extended the check to also include a check for variables with incomplete object type that are not arrays, that have an initializer. Furthermore the warning includes the type and variable name. * Warning for incomplete type in compound literals. Incomplete types are not allowed for compound literals, except for array types. * Extend type printing function. The type of a typedeof of an anonymous type should not be printed. Furthermore added '<anonymous>' to the printing of anonymous types. * Unify incomplete type errors message. The incomplete type error messages should all look the same including name of the variable, parameter, etc. and then the incomplete type.
* Functions that are extern should stay extern (#201)Bernhard Schommer2019-09-251-1/+1
| | | | | | In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier). Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
* AArch64 portXavier Leroy2019-08-082-0/+6
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+36
| | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
* Remove the cparser/Builtins moduleXavier Leroy2019-07-1712-87/+62
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* Change condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| | | | | | The warning should only be active if the optimization is active, so the check is only performed when the warning is active and additionally the command line flag -Obranchless is specified.
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-1/+1
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0519-3635/+472
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
* Deref is not safe.Bernhard Schommer2019-07-041-1/+1
|
* Added new diagnostic for non-linear conditionalsBernhard Schommer2019-07-046-1/+179
| | | | | | | | | | | | | | The new diagnostics is triggered if a conditional is used that may not be transformed into linear code by the later by the if conversion. The new diagnostic is emitted if a conditional may contain an unsafe expression or is contained within another conditional, logical and or logical or expression. An expression is unsafe if it contains a call, changes memory or if its evaluation leads to undefined behavior, for example division and modulo. Also fixes a small typo in a comment in Cutil.
* Added helper function for array types.Bernhard Schommer2019-07-042-0/+7
| | | | | The function determines whether the given type is an array type or not.
* Added statement traversal functions.Bernhard Schommer2019-07-041-107/+90
| | | | | | Refactored the checks functions by using higher order traversal functions for statements. Also introduce helper functions for the traversal of initializers.
* New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
| | | | There should only be one unnamed parameter of type void in the parameter list.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-315-9/+9
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
* Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
| | | | | | | | | | | | Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later.
* Change to AbsInt version string.Bernhard Schommer2019-05-101-1/+1
| | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
* Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
| | | | | | `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this.
* Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
| | | | | | | | | Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards.
* Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
| | | | | Since the error formatter is not automatically flushed at program exit we need to ensure that it is flushed at exit.
* Reset scope ids later.Bernhard Schommer2019-04-161-1/+1
| | | | | | | In order to avoid adding ranges to the wrong scopes due to inlining they are numbered consecutively for the whole compilation unit. Bug 26234
* Improve overflow check for integer literals (#157)Michael Schmidt2019-03-201-2/+4
| | | | | | The previous check was incomplete for integer literals in base 10. Bug 26119
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-251-6/+21
| | | | | | | | | | | | | | | | | | Consider: ``` struct s { ... } __attribute((aligned(N))); struct t { ... } __attribute((aligned(N))) struct t x; ``` In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned. In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning. This commit changes the attachment rule so that it treats both cases right. Extend regression test for "aligned" attribute accordingly, by testing aligned attribute applied to a name of struct type.
generated by cgit (git 2.34.1) at 2024-06-28 21:04:12 +0000