ltldo: add option --errors
* bin/ltldo.cc: Implement --errors. * tests/core/ltldo.test: Test it. * NEWS: Mention it.
This commit is contained in:
parent
f904c0e05c
commit
7d930359c1
3 changed files with 75 additions and 19 deletions
5
NEWS
5
NEWS
|
|
@ -1,5 +1,10 @@
|
||||||
New in spot 2.0a (not yet released)
|
New in spot 2.0a (not yet released)
|
||||||
|
|
||||||
|
Command-line tools:
|
||||||
|
|
||||||
|
* ltldo has a new option --errors=... to specify how to deal
|
||||||
|
with errors from executed tools.
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
* The print_hoa() function will now output version 1.1 of the HOA
|
* The print_hoa() function will now output version 1.1 of the HOA
|
||||||
|
|
|
||||||
80
bin/ltldo.cc
80
bin/ltldo.cc
|
|
@ -26,6 +26,7 @@
|
||||||
#include <sys/wait.h>
|
#include <sys/wait.h>
|
||||||
|
|
||||||
#include "error.h"
|
#include "error.h"
|
||||||
|
#include "argmatch.h"
|
||||||
|
|
||||||
#include "common_setup.hh"
|
#include "common_setup.hh"
|
||||||
#include "common_cout.hh"
|
#include "common_cout.hh"
|
||||||
|
|
@ -48,8 +49,16 @@ const char argp_program_doc[] ="\
|
||||||
Run LTL/PSL formulas through another program, performing conversion\n\
|
Run LTL/PSL formulas through another program, performing conversion\n\
|
||||||
of input and output as required.";
|
of input and output as required.";
|
||||||
|
|
||||||
|
enum {
|
||||||
|
OPT_ERRORS = 256,
|
||||||
|
};
|
||||||
|
|
||||||
static const argp_option options[] =
|
static const argp_option options[] =
|
||||||
{
|
{
|
||||||
|
{ nullptr, 0, nullptr, 0, "Error handling:", 4 },
|
||||||
|
{ "errors", OPT_ERRORS, "abort|warn|ignore", 0,
|
||||||
|
"how to deal with tools returning with non-zero exit codes or "
|
||||||
|
"automata that ltldo cannot parse (default: abort)", 0 },
|
||||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||||
};
|
};
|
||||||
|
|
@ -98,13 +107,32 @@ build_percent_list()
|
||||||
return &more_o_format_argp;
|
return &more_o_format_argp;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum errors_type { errors_abort, errors_warn, errors_ignore };
|
||||||
|
static errors_type errors_opt;
|
||||||
|
|
||||||
|
static char const *const errors_args[] =
|
||||||
|
{
|
||||||
|
"stop", "abort",
|
||||||
|
"warn", "print",
|
||||||
|
"ignore", "silent", nullptr
|
||||||
|
};
|
||||||
|
|
||||||
|
static errors_type const errors_types[] =
|
||||||
|
{
|
||||||
|
errors_abort, errors_abort,
|
||||||
|
errors_warn, errors_warn,
|
||||||
|
errors_ignore, errors_ignore
|
||||||
|
};
|
||||||
|
|
||||||
|
ARGMATCH_VERIFY(errors_args, errors_types);
|
||||||
|
|
||||||
const struct argp_child children[] =
|
const struct argp_child children[] =
|
||||||
{
|
{
|
||||||
{ &hoaread_argp, 0, "Parsing of automata:", 3 },
|
{ &hoaread_argp, 0, "Parsing of automata:", 3 },
|
||||||
{ &finput_argp, 0, nullptr, 1 },
|
{ &finput_argp, 0, nullptr, 1 },
|
||||||
{ &trans_argp, 0, nullptr, 3 },
|
{ &trans_argp, 0, nullptr, 3 },
|
||||||
{ &aoutput_argp, 0, nullptr, 4 },
|
{ &aoutput_argp, 0, nullptr, 5 },
|
||||||
{ build_percent_list(), 0, nullptr, 5 },
|
{ build_percent_list(), 0, nullptr, 6 },
|
||||||
{ &misc_argp, 0, nullptr, -1 },
|
{ &misc_argp, 0, nullptr, -1 },
|
||||||
{ nullptr, 0, nullptr, 0 }
|
{ nullptr, 0, nullptr, 0 }
|
||||||
};
|
};
|
||||||
|
|
@ -114,6 +142,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
{
|
{
|
||||||
switch (key)
|
switch (key)
|
||||||
{
|
{
|
||||||
|
case OPT_ERRORS:
|
||||||
|
errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types);
|
||||||
|
break;
|
||||||
case ARGP_KEY_ARG:
|
case ARGP_KEY_ARG:
|
||||||
translators.push_back(arg);
|
translators.push_back(arg);
|
||||||
break;
|
break;
|
||||||
|
|
@ -150,59 +181,64 @@ namespace
|
||||||
duration = sw.stop();
|
duration = sw.stop();
|
||||||
|
|
||||||
spot::twa_graph_ptr res = nullptr;
|
spot::twa_graph_ptr res = nullptr;
|
||||||
|
problem = false;
|
||||||
if (timed_out)
|
if (timed_out)
|
||||||
{
|
{
|
||||||
problem = false; // A timeout is considered benign
|
// A timeout is considered benign
|
||||||
std::cerr << "warning: timeout during execution of command \""
|
std::cerr << "warning: timeout during execution of command \""
|
||||||
<< cmd << "\"\n";
|
<< cmd << "\"\n";
|
||||||
++timeout_count;
|
++timeout_count;
|
||||||
}
|
}
|
||||||
else if (WIFSIGNALED(es))
|
else if (WIFSIGNALED(es))
|
||||||
{
|
{
|
||||||
problem = true;
|
if (errors_opt != errors_ignore)
|
||||||
es = WTERMSIG(es);
|
{
|
||||||
std::cerr << "error: execution of command \"" << cmd
|
problem = true;
|
||||||
<< "\" terminated by signal " << es << ".\n";
|
es = WTERMSIG(es);
|
||||||
|
std::cerr << "error: execution of command \"" << cmd
|
||||||
|
<< "\" terminated by signal " << es << ".\n";
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
|
else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
|
||||||
{
|
{
|
||||||
problem = true;
|
if (errors_opt != errors_ignore)
|
||||||
es = WEXITSTATUS(es);
|
{
|
||||||
std::cerr << "error: execution of command \"" << cmd
|
problem = true;
|
||||||
<< "\" returned exit code " << es << ".\n";
|
es = WEXITSTATUS(es);
|
||||||
|
std::cerr << "error: execution of command \"" << cmd
|
||||||
|
<< "\" returned exit code " << es << ".\n";
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else if (output.val())
|
else if (output.val())
|
||||||
{
|
{
|
||||||
problem = false;
|
|
||||||
auto aut = spot::parse_aut(output.val()->name(), dict,
|
auto aut = spot::parse_aut(output.val()->name(), dict,
|
||||||
spot::default_environment::instance(),
|
spot::default_environment::instance(),
|
||||||
opt_parse);
|
opt_parse);
|
||||||
if (!aut->errors.empty())
|
if (!aut->errors.empty() && errors_opt != errors_ignore)
|
||||||
{
|
{
|
||||||
problem = true;
|
problem = true;
|
||||||
std::cerr << "error: failed to parse the automaton "
|
std::cerr << "error: failed to parse the automaton "
|
||||||
"produced by \"" << cmd << "\".\n";
|
"produced by \"" << cmd << "\".\n";
|
||||||
aut->format_errors(std::cerr);
|
aut->format_errors(std::cerr);
|
||||||
res = nullptr;
|
|
||||||
}
|
}
|
||||||
else if (aut->aborted)
|
else if (aut->aborted && errors_opt != errors_ignore)
|
||||||
{
|
{
|
||||||
problem = true;
|
problem = true;
|
||||||
std::cerr << "error: command \"" << cmd
|
std::cerr << "error: command \"" << cmd
|
||||||
<< "\" aborted its output.\n";
|
<< "\" aborted its output.\n";
|
||||||
res = nullptr;
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
res = aut->aut;
|
res = aut->aut;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else // No automaton output
|
// Note that res can stay empty if no automaton was output.
|
||||||
|
|
||||||
|
if (problem && errors_opt == errors_ignore)
|
||||||
{
|
{
|
||||||
problem = false;
|
problem = false;
|
||||||
res = nullptr;
|
res = nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
output.cleanup();
|
output.cleanup();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
@ -280,7 +316,13 @@ namespace
|
||||||
double translation_time;
|
double translation_time;
|
||||||
auto aut = runner.translate(t, problem, translation_time);
|
auto aut = runner.translate(t, problem, translation_time);
|
||||||
if (problem)
|
if (problem)
|
||||||
error_at_line(2, 0, filename, linenum, "aborting here");
|
{
|
||||||
|
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");
|
||||||
|
}
|
||||||
if (aut)
|
if (aut)
|
||||||
{
|
{
|
||||||
if (relmap)
|
if (relmap)
|
||||||
|
|
|
||||||
|
|
@ -134,5 +134,14 @@ test $? = 2
|
||||||
grep ':.*empty input' stderr
|
grep ':.*empty input' stderr
|
||||||
grep 'ltldo: aborting' stderr
|
grep 'ltldo: aborting' stderr
|
||||||
|
|
||||||
|
$ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr
|
||||||
|
test $? = 0
|
||||||
|
test -z "`cat stderr`"
|
||||||
|
|
||||||
|
$ltldo ': %s; true>%O' --errors=warn -f GFa 2>stderr
|
||||||
|
test $? = 0
|
||||||
|
grep ':.*empty input' stderr
|
||||||
|
|
||||||
|
|
||||||
$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
|
$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
|
||||||
grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr
|
grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue