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

@@ -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();
+		    global_error()  << "error: aborted HOA file.\n";
-		    err << "error: aborted HOA file.\n";
 		    end_error();
 		    res = nullptr;
 		  }

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;

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`

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