From 519f5e3cee685af980c0ac4a15f9ed4c678863ce Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 20 Mar 2015 18:01:14 +0100
Subject: [PATCH] hoa: fix an assert() when initial states are not declared

* src/hoaparse/hoaparse.yy: Make sure initial states are
declared.
* src/tgbatest/hoaparse.test: Test it.
---
 src/hoaparse/hoaparse.yy   | 27 ++++++++++++++++++++-------
 src/tgbatest/hoaparse.test | 33 ++++++++++++++++++++++++++++++++-
 2 files changed, 52 insertions(+), 8 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 2f356214f..88ff09184 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -727,6 +727,12 @@ acceptance-cond: IDENTIFIER '(' acc-set ')'
 
 
 body: states
+      {
+	for (auto& p: res.start)
+	  if (p.second >= res.declared_states.size()
+	      || !res.declared_states[p.second])
+	    error(p.first, "no definition for this initial state");
+      }
 
 state-num: INT
 	   {
@@ -1059,6 +1065,7 @@ never: "never" { res.namer = res.h->aut->create_namer<std::string>();
 	 // states to remove.
 	 if (res.aliased_states)
 	   res.h->aut->purge_unreachable_states();
+	 res.declared_states.resize(res.h->aut->num_states(), true);
        }
 
 nc-states:
@@ -1262,8 +1269,8 @@ lbtt: lbtt-header lbtt-body ENDAUT
 	  }
 	if (res.states_map.rbegin()->first > (unsigned) res.states)
 	  {
-	    // We have seen number larger that the total number of
-	    // state in the automaton.  Usually this happens when the
+	    // We have seen numbers larger that the total number of
+	    // states in the automaton.  Usually this happens when the
 	    // states are numbered from 1 instead of 0, but the LBTT
 	    // documentation actually allow any number to be used.
 	    // What we have done is to map all input state numbers 0
@@ -1281,6 +1288,7 @@ lbtt: lbtt-header lbtt-body ENDAUT
 	      i.second = rename[i.second];
 	    res.h->aut->get_graph().defrag_states(std::move(rename), s);
 	  }
+	 res.declared_states.resize(res.h->aut->num_states(), true);
       }
     | lbtt-header-states LBTT_EMPTY
       {
@@ -1538,7 +1546,16 @@ static void fix_acceptance(result_& r)
 
 static void fix_initial_state(result_& r)
 {
-  if (r.start.empty())
+
+  std::vector<unsigned> start;
+  start.reserve(r.start.size());
+  for (auto& p : r.start)
+    // Ignore initial states without declaration
+    if (p.second < r.declared_states.size()
+	&& r.declared_states[p.second])
+      start.push_back(p.second);
+
+  if (start.empty())
     {
       // If no initial state has been declared, add one, because
       // Spot will not work without one.
@@ -1547,10 +1564,6 @@ static void fix_initial_state(result_& r)
     }
 
   // Remove any duplicate initial state.
-  std::vector<unsigned> start;
-  start.reserve(r.start.size());
-  for (auto& p : r.start)
-    start.push_back(p.second);
   std::sort(start.begin(), start.end());
   auto res = std::unique(start.begin(), start.end());
   start.resize(std::distance(start.begin(), res));
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 2988b169d..7d9e663d1 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -26,8 +26,12 @@ set -e
 expecterr()
 {
    cat >$1.exp
-   ../../bin/autfilt --hoa "$@" 2>$1.err >$1.out && exit 1
+   ../../bin/autfilt --hoa "$@" 2>$1.err-t >$1.out && exit 1
    test $? = 2
+   # If autfilt is compiled statically, the '.../lt-' parse of
+   # its name is not stripped, and the error message show the
+   # full path.
+   sed 's:^\.\./\.\./bin/::' $1.err-t >$1.err
    cat $1.err
    diff $1.err $1.exp
 }
@@ -164,6 +168,7 @@ input:3.1-9: ... declared here.
 input:6.10-14: ignoring acceptance sets because of missing acceptance condition
 input:7.5: state number is larger than state count...
 input:3.1-9: ... declared here.
+input:4.1-8: no definition for this initial state
 EOF
 
 cat >input <<EOF
@@ -179,6 +184,7 @@ expecterr input <<EOF
 input:3.1-8: initial state number is larger than state count...
 input:4.1-9: ... declared here.
 input:1.1-4.9: missing 'Acceptance:' header
+input:3.1-8: no definition for this initial state
 EOF
 
 cat >input <<EOF
@@ -194,6 +200,7 @@ EOF
 expecterr input <<EOF
 input:5.1-13: ignoring this redefinition of the acceptance condition...
 input:2.1-13: ... previously defined here.
+input:3.1-8: no definition for this initial state
 EOF
 
 cat >input <<EOF
@@ -956,6 +963,7 @@ input:21.5-7: $se string, expecting integer
 input:25.1: $se \$undefined, expecting $end
 input:25.1-12: ignoring leading garbage
 input:32.1-5: $se header name, expecting --END-- or State:
+input:28.1-8: no definition for this initial state
 input:37.1: $se 't', expecting $end
 autfilt: failed to read automaton from input
 EOF
@@ -1548,3 +1556,26 @@ State: 5 {0 1}
 2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5
 --END--
 EOF
+
+
+# This used to trigger an assertion.
+cat >bug<<EOF
+HOA: v1
+Start: 6
+Acceptance: 0 t
+--BODY--
+--END--
+HOA: v1
+Start: 1
+Start: 0
+Acceptance: 0 t
+--BODY--
+State: 0
+[t] 0
+--END--
+EOF
+
+expecterr bug <<EOF
+bug:2.1-8: no definition for this initial state
+bug:7.1-8: no definition for this initial state
+EOF