aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Lexer.mll
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-011-1/+1
|\
| * Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
| | | | | | | | | | | | | | Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+2
|\| | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | | | | | | | | | All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially.
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-0/+2
|\|
| * Support _Static_assert from C11Xavier Leroy2020-07-211-0/+2
| |
* | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-251-1/+1
|\|
| * 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.
* | parse _Thread_localDavid Monniaux2020-02-241-0/+2
|/
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-127/+120
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* 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.
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-141-1/+1
| | | | | | | | | | | | | | | | | | * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-3/+3
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-5/+5
| | | | | | | | | | | | | | | | | * 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.
* Remove unused open.Bernhard Schommer2017-02-061-1/+0
|
* Implement offsetof via builtin.Bernhard Schommer2017-01-201-0/+2
| | | | | | | | | | | | 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
* Classified all warnings and added various options.Bernhard Schommer2016-07-291-6/+6
| | | | | | | | | | 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
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-0/+2
| | | | | | | | 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-1/+1
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Code cleanup.Bernhard Schommer2016-03-101-4/+3
| | | | | | 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.
* 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.
* Merge pull request #69 from jhjourdan/parser_fixBernhard Schommer2015-11-121-39/+40
|\ | | | | Parser : duplicate identifier tokens, fix K&R definition parsing
| * Merge remote-tracking branch 'origin/master' into parser_fixJacques-Henri Jourdan2015-11-041-29/+62
| |\
| * | other, simpler fix: the lexer emits 2 tokens for each identifierJacques-Henri Jourdan2015-10-081-40/+40
| | |
* | | Change one line in [Lexer.mll] to obey API change in Menhir 20151110.François Pottier2015-11-101-1/+1
| |/ |/| | | | | Update configure to require Menhir 20151110.
* | Install the new system for reporting syntax errors.François Pottier2015-10-231-6/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This requires the development version of Menhir, to be released soon. In summary: handcrafted.messages is new. It contains a mapping of erroneous sentences to error messages, together with a lot of comments. Makefile.extr is new. It contains a rule to generate cparser/pre_parser_messages.ml based on this mapping. cparser/ErrorReports.{ml,mli} are new. They construct syntax error messages, based on the compiled mapping. cparser/Lexer.mll is modified. The last two tokens that have been read are stored in a buffer. ErrorReports is called to construct a syntax error message. cparser/GNUmakefile is new. It offers several commands for working on the pre-parser. cparser/deLexer.ml is new. It is a script (it is not linked into CompCert). It translates the symbolic name of a token to an example of this token in concrete C syntax. It is used by [make -C cparser concrete] to produce the .c files in tests/generated/. cparser/tests/generated/Makefile is new. It runs ccomp, clang and gcc on each of the generated C files, so as to allow a comparison of the error messages.
* | Lexer update: use Menhir's incremental API instead of Menhir's traditional API.François Pottier2015-10-231-3/+16
| | | | | | | | | | This means that CompCert must now be compiled in --table mode. At this point, the error message for a syntax error is still just "syntax error".
* | Lexer cleanup: isolate [lexer_wraper] and rename it to [lexer].François Pottier2015-10-231-6/+10
| |
* | Lexer cleanup: isolate the entry point into the lexer.François Pottier2015-10-231-6/+10
| |
* | Read the whole source C file into memory instad of reading it on demand.François Pottier2015-10-231-2/+2
| | | | | | | | | | Having the file in memory will help build an error message. Also, this may be slightly faster.
* | Fix [Lexer.char_literal] and [Lexer.string_literal] to properly keep track ↵François Pottier2015-10-221-10/+12
|/ | | | | | of [lex_start_p]. This is required for Menhir to pick up the correct start position of the token.
* Fixed a few bugs in the pre parser. In particular, the following codeJacques-Henri Jourdan2015-09-301-36/+42
| | | | | | | | | | | | | | | 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.
* Detect (and reject with an error) preprocessing numbers that are not valid ↵Xavier Leroy2015-04-061-0/+7
| | | | integer or floating constants.
* Recognize more of GCC's alternate keywords (e.g. "__signed").Xavier Leroy2014-12-291-21/+24
| | | | | Based on the source of GCC 4.9.2. Plus: reordered keywords in alphabetic order to facilitate comparison.
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
| | | | | These alternate keywords for "volatile" are used in some header files in the wild.
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-211-1/+1
| | | | | | | | The previous behavior for illegal escape sequences (e.g. '\%') in character and string literals was to emit an error, then treat "\x" as "x". As reported by a user, this is dangerous, because the warning can go unnoticed, and other compilers can treat "\x" as "\\x" (backslash followed by 'x'). Better to error out.
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-121-62/+101
| | | | | | | | | | - 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
* Fix string litteral parsingjjourdan2014-05-111-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2490 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Added alternate keywords __inline, __restrict, etc, for GCC compatibilityxleroy2014-05-081-2/+24
| | | | | | | - Skip comments that might remain after preprocessing git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2487 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat all identifiers as VAR_NAME by default (i.e. if not bound by a ↵xleroy2014-05-051-12/+7
| | | | | | typedef). This produces better error messages for unbound variable names (proper error message in Elab rather than cryptic syntax error in pre_parser). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2477 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Be less picky in the way we parse '#' linesxleroy2014-05-021-11/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-593/+462
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "alignas" branch.xleroy2013-10-051-0/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-18/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 'typeof' is not a keywordxleroy2012-02-291-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1829 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+1
| | | | | | | | | | and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-0/+604
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-19 21:55:46 +0000