diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 187bb4401..181aa87e0 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -849,9 +849,9 @@ nc-formula: nc-formula-or-ident // 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; + 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; + here.begin.column += j.first.begin.column - 1; error_list.emplace_back(here, j.second); } bdd cond = bddfalse; diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 4f5dc7858..61115fa0b 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -300,6 +300,36 @@ cat stderr grep input: stderr > stderrfilt diff stderrfilt expected-err + +# Empty guards should be diagnosed at the correct location +cat >input < goto accept_all + :: ( ) -> goto T0_init + fi; +accept_all: + skip +} +EOF +run 2 ../../bin/autfilt --dot stdout 2>stderr +grep '5.6-8: unexpected empty block' stderr + +cat >expected < 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<