From 676ab41f6f0ae5e732e0da57bfada16e10ff1cff Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 18 Oct 2012 00:23:34 +0200
Subject: [PATCH] ltlparse: diagnose empty (...) block in lenient mode.

* src/ltlparse/ltlparse.yy (try_recursive_parse): Diagnose
empty strings.
* src/ltltest/lenient.test: Add tests.
---
 src/ltlparse/ltlparse.yy | 10 +++++++++-
 src/ltltest/lenient.test |  7 +++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index e99c36f2f..5de0d232e 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -108,6 +108,14 @@ using namespace spot::ltl;
       // Otherwise, we convert the string into an atomic proposition
       // (it's up to the environment to check the syntax of this
       // proposition, and maybe reject it).
+
+      if (str.empty())
+	{
+	  error_list.push_back(parse_error(location,
+					   "unexpected empty block"));
+	  return 0;
+	}
+
       spot::ltl::parse_error_list suberror;
       const spot::ltl::formula* f;
       if (sere)
@@ -802,7 +810,7 @@ subformula: booleanatom
 		delete $1;
 		if (!$$)
 		  YYERROR;
-	        $$ = binop::instance(binop::EConcat, $$,
+		$$ = binop::instance(binop::EConcat, $$,
 				     constant::true_instance());
 	      }
 
diff --git a/src/ltltest/lenient.test b/src/ltltest/lenient.test
index b6dc8b6ff..a39aeb9ea 100755
--- a/src/ltltest/lenient.test
+++ b/src/ltltest/lenient.test
@@ -33,6 +33,7 @@ cat >input <<EOF
 (((a < b ) U ({(  b == c - 1  )})))
 (((((  a < b))) U ( b == c - 1)))
 (((((  a < b))) U { b == c - 1}!))
+()a
 EOF
 
 cat >expected <<EOF
@@ -44,7 +45,13 @@ cat >expected <<EOF
 "a < b" U "b == c - 1"
 "a < b" U "b == c - 1"
 "a < b" U "b == c - 1"
+Xa
 EOF
 
 run 0 $ltlfilt --lenient input > output
 cmp output expected
+
+
+
+run 2 $ltlfilt --lenient -f 'F( )' 2> stderr
+grep 'unexpected empty block' stderr
\ No newline at end of file