From ebc3d649270fc62943bb0b943709107300bcff00 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 4 Dec 2014 08:36:59 +0100
Subject: [PATCH] neverclaim: fix reporting of parse_boolean() errors

* src/hoaparse/hoaparse.yy: Correctly adjust the
location of error messagges.
* src/tgbatest/neverclaimread.test: Add test case.
---
 src/hoaparse/hoaparse.yy         |  4 ++--
 src/tgbatest/neverclaimread.test | 30 ++++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 2 deletions(-)

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 <<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
 a
 FG a