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