Commit 63abfed1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: report aborted HOA files

* src/bin/ltlcross.cc: Here.
* src/tgbatest/ltlcross3.test: Add test case.
parent c12b2d63
......@@ -1055,6 +1055,16 @@ namespace
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";
end_error();
res = nullptr;
}
else
{
res = aut->aut;
......
......@@ -130,3 +130,13 @@ check_csv out.csv
grep 'X a' bug.txt
test $q -eq `expr $p + 6`
# Support for --ABORT-- in HOA.
run 1 ../../bin/ltlcross 'echo HOA: --ABORT-- %f > %H' \
-f a --csv=out.csv 2>stderr
grep '"exit_status"' out.csv
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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment