aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Parser.vy
Commit message (Collapse)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
| | | | cfrontend/C2C.ml
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+18
|\
| * Support _Static_assert from C11Xavier Leroy2020-07-211-1/+18
| |
* | parse _Thread_localDavid Monniaux2020-02-241-1/+3
|/
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-289/+306
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Wrong AST for GCC-style attributesXavier Leroy2018-08-171-1/+1
| | | | | The list of arguments to the attribute was missing a reverse, hence attribute(("foo"(1,2,3))) was actually read as attribute(("foo"(3,2,1))).
* Remove the `_Alignas(expr)` construct (#125)Xavier Leroy2018-06-071-4/+2
| | | | The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
* Change the syntax to gcc/clangs syntax.Bernhard Schommer2017-02-011-2/+4
| | | | | | This only means that there must be one identifier at the begining and then a designator. Bug 20765
* New version to support designators.Bernhard Schommer2017-01-241-2/+2
| | | | | | | | | 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
* Implement offsetof via builtin.Bernhard Schommer2017-01-201-1/+3
| | | | | | | | | | | | 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
* Keep anonymous members of anonymous structs.Bernhard Schommer2016-09-271-1/+1
| | | | | The anonymous members are kept but using them is still an error. Bug 19907
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-9/+10
| | | | | | | | 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
* Better handling of old-style K&R function declarations:Jacques-Henri Jourdan2015-11-011-67/+79
| | | | | | - 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
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-4/+50
|
* Support "asm volatile" (closes: PR#5).Xavier Leroy2014-12-291-0/+2
| | | | The CompCert back-end already treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable side-effects), so no change is required outside of the parser.
* Empty declarationsjjourdan2014-05-231-0/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-151-2/+2
| | | | | | | | - Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-121-2/+6
| | | | | | | | | | - Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for old-style K&R function definitions.xleroy2014-05-051-2/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2478 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-0/+845
(Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 01:13:35 +0000