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

ltlcross: fix --verbose --no-check crash

Browse source 
Report from František Blahoudek.

* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-13 13:53:42 +02:00
parent ad502eb324
commit cc1191cd66
3 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -32,6 +32,8 @@ New in spot 2.1.1.dev (not yet released)
* Fix python errors on Darwin when using methods from the spot module * Fix python errors on Darwin when using methods from the spot module
inside of the spot.ltsmin submodule. inside of the spot.ltsmin submodule.
* Fix ltlcross crash when combining --no-check with --verbose.
New in spot 2.1.1 (2016-09-20) New in spot 2.1.1 (2016-09-20)
Command-line tools: Command-line tools:

4
bin/ltlcross.cc
View file

@ -1066,6 +1066,8 @@ namespace
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i, auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char prefix) const char prefix)
{ {
if (!x[i])
return;
std::cerr << "info: " << prefix << i << "\t("; std::cerr << "info: " << prefix << i << "\t(";
printsize(x[i]); printsize(x[i]);
std::cerr << ')'; std::cerr << ')';
@ -1094,7 +1096,7 @@ namespace
std::vector<spot::twa_graph_ptr>& to, unsigned i, std::vector<spot::twa_graph_ptr>& to, unsigned i,
char prefix) char prefix)
{ {
if (!to[i]) if (from[i] && !to[i])
{ {
if (print_first) if (print_first)
{ {

8
tests/core/ltlcross3.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et # Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
# Développement de l'Epita (LRDE). # et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -180,3 +180,7 @@ cat >expected<<EOF
% %
EOF EOF
diff foo expected diff foo expected
# This command used to crash. Report from František Blahoudek.
run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'