diff --git a/NEWS b/NEWS index a485d33f9..eb833532f 100644 --- a/NEWS +++ b/NEWS @@ -58,6 +58,9 @@ New in spot 2.9.0.dev (not yet released) every place where 0 occur, and then the acceptance would be renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed. + - Improve ltldo diagnostics to fix spurious test-suite failure on + systems with antique GNU libc. + New in spot 2.9 (2020-04-30) Command-line tools: diff --git a/bin/ltldo.cc b/bin/ltldo.cc index fdb634450..f57a528b2 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -39,6 +39,7 @@ #include "common_hoaread.hh" #include +#include #include #include #include @@ -233,18 +234,13 @@ namespace problem = false; if (timed_out) { - // A timeout is considered benign + // A timeout is considered benign, unless --fail-on-timeout. if (fail_on_timeout) - { - std::cerr << "error:"; - problem = true; - } + problem = true; else - { - std::cerr << "warning:"; - ++timeout_count; - } - std::cerr << " timeout during execution of command \"" + ++timeout_count; + std::cerr << program_name + << ": timeout during execution of command \"" << cmd << "\"\n"; } else if (WIFSIGNALED(es)) @@ -253,7 +249,7 @@ namespace { problem = true; es = WTERMSIG(es); - std::cerr << "error: execution of command \"" << cmd + std::cerr << program_name << ": execution of command \"" << cmd << "\" terminated by signal " << es << ".\n"; } } @@ -263,7 +259,7 @@ namespace { problem = true; es = WEXITSTATUS(es); - std::cerr << "error: execution of command \"" << cmd + std::cerr << program_name << ": execution of command \"" << cmd << "\" returned exit code " << es << ".\n"; } } @@ -275,14 +271,14 @@ namespace if (!aut->errors.empty() && errors_opt != errors_ignore) { problem = true; - std::cerr << "error: failed to parse the automaton " + std::cerr << program_name << ": failed to parse the automaton " "produced by \"" << cmd << "\".\n"; aut->format_errors(std::cerr); } else if (aut->aborted && errors_opt != errors_ignore) { problem = true; - std::cerr << "error: command \"" << cmd + std::cerr << program_name << ": command \"" << cmd << "\" aborted its output.\n"; } else @@ -410,11 +406,14 @@ namespace auto aut = runner.translate(t, problem, timer); if (problem) { - if (errors_opt == errors_abort) - error_at_line(2, 0, filename, linenum, "aborting here"); - else - error_at_line(0, 0, filename, linenum, - "failed to translate this input"); + // An error message already occurred about the problem, + // but this additional one will print filename & + // linenum, and possibly exit. + std::string sf = spot::str_psl(f); + error_at_line(errors_opt == errors_abort ? 2 : 0, 0, + filename, linenum, + "failed to run `%s' on `%s'", + tools[t].name, sf.c_str()); } if (aut) { diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index 601f9329d..ce02dfb04 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -43,21 +43,23 @@ genltl --or-g=1..2 | run 0 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ >output 2>stderr test -z "`cat output`" -test 4 = `grep -c warning: stderr` +test 4 = `grep -c ltldo: stderr` +grep -q 'failed to' stderr && exit 1 genltl --or-g=1..2 | run 0 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ --fail-on-timeout --error=warn >output 2>stderr test -z "`cat output`" -test 4 = `grep -c error: stderr` -grep -q 'aborting here' stderr && exit 1 +test 8 = `grep -c ltldo: stderr` +test 4 = `grep -c ltldo:-: stderr` +grep -q 'failed to' stderr genltl --or-g=1..2 | run 2 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ --fail-on-timeout >output 2>stderr test -z "`cat output`" -test 1 = `grep -c error: stderr` -grep -q 'aborting here' stderr +test 2 = `grep -c ltldo: stderr` +grep -q 'failed to' stderr test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4' @@ -143,7 +145,7 @@ diff output expected ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1 test $? = 2 grep ':.*empty input' stderr -grep 'ltldo: aborting' stderr +grep 'ltldo: failed to run' stderr ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr test $? = 0