hoaparse: improve reporting of errors in LBTT guards
* src/hoaparse/hoaparse.yy: forward the error messages from lbt_parse(). * src/hoaparse/hoascan.ll: Minor cleanups. * src/tgbatest/lbttparse.test: Test it.
This commit is contained in:
parent
f9e859d765
commit
1a022c8093
3 changed files with 34 additions and 9 deletions
|
|
@ -991,11 +991,20 @@ lbtt-guard: STRING
|
||||||
spot::ltl::parse_error_list pel;
|
spot::ltl::parse_error_list pel;
|
||||||
auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env);
|
auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env);
|
||||||
if (!f || !pel.empty())
|
if (!f || !pel.empty())
|
||||||
|
error(@$, "failed to parse guard");
|
||||||
|
if (!pel.empty())
|
||||||
|
for (auto& j: pel)
|
||||||
|
{
|
||||||
|
// Adjust the diagnostic to the current position.
|
||||||
|
spot::location here = @1;
|
||||||
|
here.end.line = here.begin.line + j.first.end.line - 1;
|
||||||
|
here.end.column = here.begin.column + j.first.end.column - 1;
|
||||||
|
here.begin.line += j.first.begin.line - 1;
|
||||||
|
here.begin.column += j.first.begin.column - 1;
|
||||||
|
error_list.emplace_back(here, j.second);
|
||||||
|
}
|
||||||
|
if (!f)
|
||||||
{
|
{
|
||||||
// FIXME: show pel.
|
|
||||||
error(@$, "failed to parse guard");
|
|
||||||
if (f)
|
|
||||||
f->destroy();
|
|
||||||
res.cur_label = bddtrue;
|
res.cur_label = bddtrue;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -34,7 +34,6 @@ typedef hoayy::parser::token token;
|
||||||
static unsigned comment_level = 0;
|
static unsigned comment_level = 0;
|
||||||
static unsigned parent_level = 0;
|
static unsigned parent_level = 0;
|
||||||
static int orig_cond = 0;
|
static int orig_cond = 0;
|
||||||
static bool missing_parent = false;
|
|
||||||
static bool lbtt_s = false;
|
static bool lbtt_s = false;
|
||||||
static bool lbtt_t = false;
|
static bool lbtt_t = false;
|
||||||
static unsigned lbtt_states = 0;
|
static unsigned lbtt_states = 0;
|
||||||
|
|
@ -249,9 +248,9 @@ identifier [[:alpha:]_][[:alnum:]_-]*
|
||||||
|
|
||||||
<in_COMMENT>{
|
<in_COMMENT>{
|
||||||
"/""*"+ ++comment_level;
|
"/""*"+ ++comment_level;
|
||||||
[^*/\n]* continue;
|
[^*/\n\r]* continue;
|
||||||
"/"[^*\n]* continue;
|
"/"[^*\n\r]* continue;
|
||||||
"*"+[^*/\n]* continue;
|
"*"+[^*/\n\r]* continue;
|
||||||
{eol} yylloc->lines(yyleng); yylloc->end.column = 1;
|
{eol} yylloc->lines(yyleng); yylloc->end.column = 1;
|
||||||
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
|
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
|
||||||
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond);
|
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond);
|
||||||
|
|
@ -352,7 +351,6 @@ namespace spot
|
||||||
BEGIN(INITIAL);
|
BEGIN(INITIAL);
|
||||||
comment_level = 0;
|
comment_level = 0;
|
||||||
parent_level = 0;
|
parent_level = 0;
|
||||||
missing_parent = false;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
|
|
|
||||||
|
|
@ -111,3 +111,21 @@ cat >expected<<EOF
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
diff output expected
|
diff output expected
|
||||||
|
|
||||||
|
cat > input <<EOF
|
||||||
|
1 2t
|
||||||
|
0 1
|
||||||
|
0 -1 & ! "a" ! "b" !
|
||||||
|
0 0 -1 & "a" ! "b" /* comments are OK */
|
||||||
|
0 1 -1 & ! "a" /* here too */ "b"
|
||||||
|
0 0 1 -1 & "a" "b"
|
||||||
|
-1
|
||||||
|
EOF
|
||||||
|
cat >expected <<EOF
|
||||||
|
input:3.5-20: failed to parse guard
|
||||||
|
input:3.20: syntax error, unexpected '!', expecting end of formula
|
||||||
|
input:3.20: ignoring trailing garbage
|
||||||
|
EOF
|
||||||
|
../../bin/autfilt -q input 2> stderr && exit 1
|
||||||
|
cat stderr
|
||||||
|
diff stderr expected
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue