From 63abfed1085de439a1ee36ee2eb28f781ea786d4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 21 Nov 2014 15:21:23 +0100
Subject: [PATCH] ltlcross: report aborted HOA files

* src/bin/ltlcross.cc: Here.
* src/tgbatest/ltlcross3.test: Add test case.
---
 src/bin/ltlcross.cc         | 10 ++++++++++
 src/tgbatest/ltlcross3.test | 10 ++++++++++
 2 files changed, 20 insertions(+)

diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 04bb19e32..1e3216c58 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -1055,6 +1055,16 @@ namespace
 		    end_error();
 		    res = nullptr;
 		  }
+		else if (aut->aborted)
+		  {
+		    status_str = "aborted";
+		    problem = true;
+		    es = -1;
+		    std::ostream& err = global_error();
+		    err << "error: aborted HOA file.\n";
+		    end_error();
+		    res = nullptr;
+		  }
 		else
 		  {
 		    res = aut->aut;
diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test
index 2ecfe25fb..236b83d94 100755
--- a/src/tgbatest/ltlcross3.test
+++ b/src/tgbatest/ltlcross3.test
@@ -130,3 +130,13 @@ check_csv out.csv
 grep 'X  a' bug.txt
 
 test $q -eq `expr $p + 6`
+
+
+# Support for --ABORT-- in HOA.
+run 1 ../../bin/ltlcross 'echo HOA: --ABORT-- %f > %H' \
+   -f a --csv=out.csv 2>stderr
+grep '"exit_status"' out.csv
+grep '"exit_code"' out.csv
+test `grep 'error:.*aborted' stderr | wc -l` -eq 2
+test `grep '"aborted",-1' out.csv | wc -l` -eq 2
+check_csv out.csv