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 8e9e706003
commit b7abe6f4b4
3 changed files with 31 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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