alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltldo: improve error messages

Browse source 
Use ltldo:... instead of error:... and warning:... and also improve
the diagnostic displayed after a translation failure to mention the
tool and formula.

Incidentally, this fixes a spurious test case failure observed by
Philipp Schlehuber on CentOS7.7 where glibc 2.17 is installed.  With
this system, when posix_spawn() starts a binary that does not exist,
it returns success and let the child die with exit code 127.  On more
recent glibc, posix_spawn() manages to return execve()'s errno, as if
the child had not been created.  We handle those two different ways to
fail, but before this patch one used to print "error:..." and the
other "ltldo:...".

* bin/ltldo.cc: Display the program_name in error message.  Display
the command name and formula on translation failure.
* tests/core/ltldo.test: Adjust test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-31 16:19:51 +02:00
parent 3368b4b99f
commit 4cfa253830
3 changed files with 31 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -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:

39
bin/ltldo.cc
View file

@ -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 <spot/tl/relabel.hh>
#include <spot/tl/print.hh>
#include <spot/misc/bareword.hh>
#include <spot/misc/timer.hh>
#include <spot/twaalgos/lbtt.hh>
@ -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)
{

16
tests/core/ltldo.test
View file

@ -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