You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In #41 a missing typedef for a type __uint128_t results in the following exception:
$ ./regtest.sh 00 07
./goblint --enable dbg.debug --enable dbg.showtemps --enable dbg.regression --sets warnstyle "legacy" --html tests/regression/00-sanity/07-term2.c
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/mach/arm/_structs.h[443:0-0] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")
Raised at Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 205, characters 6-39
Called from Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 124, characters 13-38
Called from Frontc.parse_helper in file "src/frontc/frontc.ml", line 256, characters 13-32
Called from Frontc.parse in file "src/frontc/frontc.ml" (inlined), line 264, characters 32-55
Called from Cilfacade.parse in file "src/util/cilfacade.ml", line 24, characters 2-26
Called from Stdlib__list.rev_map.rmap_f in file "list.ml", line 103, characters 22-25
Called from Maingoblint.merge_preprocessed in file "src/maingoblint.ml", line 256, characters 18-62
Called from Maingoblint.main in file "src/maingoblint.ml", line 460, characters 15-56
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 554, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 560, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20
There are two problems:
Little information about the input
No information about where this happened in CIL
For 1. we could print the input that has not been lexed such that one does not need to search the file for it
For 2.:
CIL re-raises Parse_error which hides the inner backtrace:
$ dune exec src/main.exe /Users/voglerr/goblint/analyzer/goblint_temp_e54e31/07-term2.c/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/mach/arm/_structs.h[443:0-0] : syntax errorParsing errorFatal error: exception Frontc.ParseError("Parse error")Raised at Errormsg.parse_error in file "src/ocamlutil/errormsg.ml", line 328, characters 2-27Called from Stdlib__parsing.yyparse.loop in file "parsing.ml", line 151, characters 8-44Called from Stdlib__parsing.yyparse in file "parsing.ml", line 164, characters 4-28Re-raised at Stdlib__parsing.yyparse in file "parsing.ml", line 183, characters 8-17Called from Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 106, characters 10-15Re-raised at Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 110, characters 1-8Called from Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 191, characters 15-90Re-raised at Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 207, characters 6-73Called from Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 124, characters 13-38Called from Frontc.parse_helper in file "src/frontc/frontc.ml", line 258, characters 13-32Called from Frontc.parse in file "src/frontc/frontc.ml", line 266, characters 32-55Called from Dune__exe__Main.parseOneFile in file "src/main.ml", line 60, characters 12-28Called from Util.count_map in file "src/ocamlutil/util.ml", line 19, characters 12-15Called from Dune__exe__Main.theMain in file "src/main.ml", line 191, characters 16-64Called from Dune__exe__Main in file "src/main.ml", line 255, characters 4-14
which is also not helpful since it has no reference to any of CIL's parsing files src/frontc/{clexer.mll, cparser.mly} (or generated files from it).
This only concerns the stack-trace. Ideally the parser would emit a helpful error - in this case that the type was not defined.
As @michael-schwarz mentioned in the original comment below, we could
So, I think the Lexer will emit an IDENT token here. It is only later during parsing that the error is recognized.
So what one would need are parser error messages that are easy for the user to understand which is in general hard for LR(1) parsers.
I don't know how to do better than report the location of the error (plus maybe the part of the input that has not been lexed?)
One could look at Menhir which is a drop-in replacement of ocamlyacc, maybe this produces more helpful error messages in case of syntax errors?
In #41 a missing
typedef
for a type__uint128_t
results in the following exception:There are two problems:
For 2.:
Parse_error
which hides the inner backtrace:cil/src/frontc/frontc.ml
Lines 201 to 205 in b2c66d3
If we change it to
we get
which is also not helpful since it has no reference to any of CIL's parsing files
src/frontc/{clexer.mll, cparser.mly}
(or generated files from it).This only concerns the stack-trace. Ideally the parser would emit a helpful error - in this case that the type was not defined.
As @michael-schwarz mentioned in the original comment below, we could
ocamlyacc
Original context:
I don't think the lexer can complain here.
How is it supposed to know that
__uint128_t
is supposed to be a type as opposed to a variable name?cil/src/frontc/clexer.mll
Lines 261 to 271 in b2c66d3
cil/src/frontc/clexer.mll
Line 583 in b2c66d3
So, I think the Lexer will emit an
IDENT
token here. It is only later during parsing that the error is recognized.So what one would need are parser error messages that are easy for the user to understand which is in general hard for LR(1) parsers.
I don't know how to do better than report the location of the error (plus maybe the part of the input that has not been lexed?)
One could look at Menhir which is a drop-in replacement of
ocamlyacc
, maybe this produces more helpful error messages in case of syntax errors?Originally posted by @michael-schwarz in #41 (comment)
The text was updated successfully, but these errors were encountered: