From 1a022c8093c8641ef4bb536aecf5c050e400e35b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 11 Dec 2014 21:43:39 +0100
Subject: [PATCH] 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.
---
 src/hoaparse/hoaparse.yy    | 17 +++++++++++++----
 src/hoaparse/hoascan.ll     |  8 +++-----
 src/tgbatest/lbttparse.test | 18 ++++++++++++++++++
 3 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 89db32899..859cccba1 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -991,11 +991,20 @@ lbtt-guard: STRING
 	    spot::ltl::parse_error_list pel;
 	    auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env);
 	    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;
 	      }
 	    else
diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll
index 1ab0390e4..91c0d62cf 100644
--- a/src/hoaparse/hoascan.ll
+++ b/src/hoaparse/hoascan.ll
@@ -34,7 +34,6 @@ typedef hoayy::parser::token token;
 static unsigned comment_level = 0;
 static unsigned parent_level = 0;
 static int orig_cond = 0;
-static bool missing_parent = false;
 static bool lbtt_s = false;
 static bool lbtt_t = false;
 static unsigned lbtt_states = 0;
@@ -249,9 +248,9 @@ identifier  [[:alpha:]_][[:alnum:]_-]*
 
 <in_COMMENT>{
   "/""*"+		++comment_level;
-  [^*/\n]*		continue;
-  "/"[^*\n]*		continue;
-  "*"+[^*/\n]*		continue;
+  [^*/\n\r]*		continue;
+  "/"[^*\n\r]*		continue;
+  "*"+[^*/\n\r]*	continue;
   {eol}			yylloc->lines(yyleng); yylloc->end.column = 1;
   {eol2}		yylloc->lines(yyleng / 2); yylloc->end.column = 1;
   "*"+"/"		if (--comment_level == 0) BEGIN(orig_cond);
@@ -352,7 +351,6 @@ namespace spot
     BEGIN(INITIAL);
     comment_level = 0;
     parent_level = 0;
-    missing_parent = false;
   }
 
   int
diff --git a/src/tgbatest/lbttparse.test b/src/tgbatest/lbttparse.test
index f48bf9dc6..f495fa58b 100755
--- a/src/tgbatest/lbttparse.test
+++ b/src/tgbatest/lbttparse.test
@@ -111,3 +111,21 @@ cat >expected<<EOF
 EOF
 
 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