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

Fully quote guards used by neverclaims.

Browse source 
Especially with should write !(p0) and not !p0, because p0 is
usually #define'd by the user and he may have forgotten to quote
the value of the macro.  This issue was discovered by Kristin
Yvonne Rozier and diagnosed by Gerard Holzmann.

* src/tgbaalgos/neverclaim.cc (process_link): Call
to_spin_string(..., true) to fully parentheses the string.
* src/tgbatest/neverclaimread.test: Add a test.
This commit is contained in:
Alexandre Duret-Lutz 2011-11-16 14:24:34 +01:00
parent 2b5956c2d4
commit ea6a1ffc22
4 changed files with 19 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
ChangeLog
View file

@ -1,3 +1,16 @@
2011-11-16 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fully quote guards used by neverclaims.
Especially with should write !(p0) and not !p0, because p0 is
usually #define'd by the user and he may have forgotten to quote
the value of the macro. This issue was discovered by Kristin
Yvonne Rozier and diagnosed by Gerard Holzmann.
* src/tgbaalgos/neverclaim.cc (process_link): Call
to_spin_string(..., true) to fully parentheses the string.
* src/tgbatest/neverclaimread.test: Add a test.
2011-11-11 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-11-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix a g++-4.7 warning about a variable used only in an assert(). Fix a g++-4.7 warning about a variable used only in an assert().

1
THANKS
View file

@ -1,6 +1,7 @@
We are grateful to these people for their comments, help, or We are grateful to these people for their comments, help, or
suggestions. suggestions.
Gerard J. Holzmann
Heikki Tauriainen Heikki Tauriainen
Jean-Michel Couvreur Jean-Michel Couvreur
Jean-Michel Ilié Jean-Michel Ilié

2
src/tgbaalgos/neverclaim.cc
View file

@ -186,7 +186,7 @@ namespace spot
os_ << " :: ("; os_ << " :: (";
const ltl::formula* f = bdd_to_formula(si->current_condition(), const ltl::formula* f = bdd_to_formula(si->current_condition(),
automata_->get_dict()); automata_->get_dict());
to_spin_string(f, os_); to_spin_string(f, os_, true);
f->destroy(); f->destroy();
state* current = si->current_state(); state* current = si->current_state();
os_ << ") -> goto " << get_state_label(current, out) << std::endl; os_ << ") -> goto " << get_state_label(current, out) << std::endl;

4
src/tgbatest/neverclaimread.test
View file

@ -118,5 +118,9 @@ do
run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba
fi fi
run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot
# Make sure there is no `!x' occurring in the
# output. Because `x' is usually #define'd, we
# should use `!(x)' in guards.
grep '![^(].*->' f.spot && exit 1
run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot
done <formulae done <formulae