alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

neverclaim: fix reporting of parse_boolean() errors

Browse source 
* src/hoaparse/hoaparse.yy: Correctly adjust the
location of error messagges.
* src/tgbatest/neverclaimread.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-04 08:36:59 +01:00
parent d0525871ed
commit ebc3d64927
2 changed files with 32 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/hoaparse/hoaparse.yy
View file

@ -849,9 +849,9 @@ nc-formula: nc-formula-or-ident
// Adjust the diagnostic to the current position. // Adjust the diagnostic to the current position.
spot::location here = @1; spot::location here = @1;
here.end.line = here.begin.line + j.first.end.line - 1; here.end.line = here.begin.line + j.first.end.line - 1;
here.end.column = here.begin.column + j.first.end.column; here.end.column = here.begin.column + j.first.end.column - 1;
here.begin.line += j.first.begin.line - 1; here.begin.line += j.first.begin.line - 1;
here.begin.column += j.first.begin.column; here.begin.column += j.first.begin.column - 1;
error_list.emplace_back(here, j.second); error_list.emplace_back(here, j.second);
} }
bdd cond = bddfalse; bdd cond = bddfalse;

30
src/tgbatest/neverclaimread.test
View file

@ -300,6 +300,36 @@ cat stderr
grep input: stderr > stderrfilt grep input: stderr > stderrfilt
diff stderrfilt expected-err diff stderrfilt expected-err
# Empty guards should be diagnosed at the correct location
cat >input <<EOF
never { /* a U b */
T0_init:
if
:: ((b)) -> goto accept_all
:: ( ) -> goto T0_init
fi;
accept_all:
skip
}
EOF
run 2 ../../bin/autfilt --dot <input >stdout 2>stderr
grep '5.6-8: unexpected empty block' stderr
cat >expected <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="0"]
1 -> 2 [label="b"]
1 -> 1 [label="0"]
2 [label="1", peripheries=2]
2 -> 2 [label="1\n{0}"]
}
EOF
diff stdout expected
cat >formulae<<EOF cat >formulae<<EOF
a a
FG a FG a