| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
|\| |
|
| |
| |
| |
| | |
Some preprocessors don't remove the vertical tab from the input
so we should be able to handle them in the lexer.
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
`_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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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"
|
|
|
|
|
|
| |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|\
| |
| | |
Parser : duplicate identifier tokens, fix K&R definition parsing
|
| |\ |
|
| | | |
|
| |/
|/|
| |
| | |
Update configure to require Menhir 20151110.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| | |
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".
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Having the file in memory will help build an error message.
Also, this may be slightly faster.
|
|/
|
|
|
|
| |
of [lex_start_p].
This is required for Menhir to pick up the correct start position of the token.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
integer or floating constants.
|
|
|
|
|
| |
Based on the source of GCC 4.9.2.
Plus: reordered keywords in alphabetic order to facilitate comparison.
|
|
|
|
|
| |
These alternate keywords for "volatile" are used in some header files
in the wild.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2490 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
- Skip comments that might remain after preprocessing
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2487 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1829 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|