rearrange some code to trigger less warning from PVS-Studio

For #192.

* spot/tl/formula.cc: Avoid calling twice the same function.
* spot/twaalgos/gtec/gtec.cc: Do not shadow a member variable.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-28 23:00:52 +02:00
parent 835b5ee1cf
commit 65955b44d9
2 changed files with 11 additions and 9 deletions

View file

@ -1276,8 +1276,9 @@ namespace spot
else else
{ {
is_.syntactic_safety = false; is_.syntactic_safety = false;
is_.syntactic_obligation = children[1]->is_syntactic_guarantee(); bool g = children[1]->is_syntactic_guarantee();
is_.syntactic_recurrence = children[1]->is_syntactic_guarantee(); is_.syntactic_obligation = g;
is_.syntactic_recurrence = g;
} }
assert(children[0]->is_sere_formula()); assert(children[0]->is_sere_formula());
assert(children[1]->is_psl_formula()); assert(children[1]->is_psl_formula());
@ -1305,8 +1306,9 @@ namespace spot
else else
{ {
is_.syntactic_guarantee = false; is_.syntactic_guarantee = false;
is_.syntactic_obligation = children[1]->is_syntactic_safety(); bool s = children[1]->is_syntactic_safety();
is_.syntactic_persistence = children[1]->is_syntactic_safety(); is_.syntactic_obligation = s;
is_.syntactic_persistence = s;
} }
assert(children[0]->is_sere_formula()); assert(children[0]->is_sere_formula());
assert(children[1]->is_psl_formula()); assert(children[1]->is_psl_formula());

View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2014, 2015 Laboratoire de Recherche et // Copyright (C) 2008, 2011, 2014, 2015, 2016 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -373,11 +373,11 @@ namespace spot
couvreur99_check_shy::dump_queue(std::ostream& os) couvreur99_check_shy::dump_queue(std::ostream& os)
{ {
os << "--- TODO ---\n"; os << "--- TODO ---\n";
unsigned pos = 0; unsigned lvl = 0;
for (auto& ti: todo) for (auto& ti: todo)
{ {
++pos; ++lvl;
os << '#' << pos << " s:" << ti.s << " n:" << ti.n os << '#' << lvl << " s:" << ti.s << " n:" << ti.n
<< " q:{"; << " q:{";
for (auto qi = ti.q.begin(); qi != ti.q.end();) for (auto qi = ti.q.begin(); qi != ti.q.end();)
{ {