From 08fbe27136d6eaf03cb3d4ee20d01a382b2eccdf Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 Feb 2015 17:46:38 +0100
Subject: [PATCH] bin: diagnose empty automata in ltlcross and ltldo

* src/bin/ltlcross.cc, src/bin/ltldo.cc: Make sure
the result of hoa_parse() is non-empty.
* src/tgbatest/ltlcross3.test, src/tgbatest/ltldo.test:
Add test cases.
---
 src/bin/ltlcross.cc         | 12 ++++++++++--
 src/bin/ltldo.cc            |  7 +++++++
 src/tgbatest/ltlcross3.test |  7 ++++++-
 src/tgbatest/ltldo.test     |  5 +++++
 4 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index d9d737ee8..d454ceb29 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -598,13 +598,21 @@ namespace
 		    end_error();
 		    res = nullptr;
 		  }
+		else if (!aut)
+		  {
+		    status_str = "empty output";
+		    problem = true;
+		    es = -1;
+		    global_error() << "error: empty output.\n";
+		    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";
+		    global_error()  << "error: aborted HOA file.\n";
 		    end_error();
 		    res = nullptr;
 		  }
diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc
index 70e5a2743..7fcf799ed 100644
--- a/src/bin/ltldo.cc
+++ b/src/bin/ltldo.cc
@@ -204,6 +204,13 @@ namespace
 		    spot::format_hoa_parse_errors(std::cerr, filename, pel);
 		    res = nullptr;
 		  }
+		else if (!aut)
+		  {
+		    problem = true;
+		    std::cerr << "error: command \"" << cmd
+			      << "\" produced an empty output.\n";
+		    res = nullptr;
+		  }
 		else if (aut->aborted)
 		  {
 		    problem = true;
diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test
index 236b83d94..946b39b4e 100755
--- a/src/tgbatest/ltlcross3.test
+++ b/src/tgbatest/ltlcross3.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+# Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -140,3 +140,8 @@ 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
+
+
+# Diagnose empty automata
+run 1 ../../bin/ltlcross ': %f >%O' -f a 2>stderr
+test 2 = `grep -c 'error: empty output.' stderr`
diff --git a/src/tgbatest/ltldo.test b/src/tgbatest/ltldo.test
index 49ae8b67d..f6f7df7fe 100755
--- a/src/tgbatest/ltldo.test
+++ b/src/tgbatest/ltldo.test
@@ -103,3 +103,8 @@ State: 0
 --END--
 EOF
 diff output expected
+
+$ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1
+test $? = 2
+grep 'error: command ".*" produced an empty output.' stderr
+grep 'ltldo: aborting' stderr