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

fix some implicit promotion from bool, as suggested by PVS-Studio

Browse source 
For #192.

* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
spot/tl/randomltl.cc, spot/twa/acc.cc, spot/twaalgos/postproc.hh: Here.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-28 22:53:29 +02:00
parent 630e90b9cc
commit 279bfa00bd
5 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/parseaut/parseaut.yy
View file

@ -2067,9 +2067,9 @@ static void fix_initial_state(result_& r)
// Multiple initial states. We might need to add a fake one, // Multiple initial states. We might need to add a fake one,
// unless one of the actual initial state has no incoming edge. // unless one of the actual initial state has no incoming edge.
auto& aut = r.h->aut; auto& aut = r.h->aut;
std::vector<unsigned> has_incoming(aut->num_states(), 0); std::vector<unsigned char> has_incoming(aut->num_states(), 0);
for (auto& t: aut->edges()) for (auto& t: aut->edges())
has_incoming[t.dst] = true; has_incoming[t.dst] = 1;
bool found = false; bool found = false;
unsigned init = 0; unsigned init = 0;

4
spot/parseaut/scanaut.ll
View file

@ -425,7 +425,7 @@ namespace spot
YY_NEW_FILE; YY_NEW_FILE;
hoayyreset(); hoayyreset();
if (want_interactive) if (want_interactive)
yy_set_interactive(true); yy_set_interactive(1);
return 0; return 0;
} }
@ -461,7 +461,7 @@ namespace spot
YY_NEW_FILE; YY_NEW_FILE;
hoayyreset(); hoayyreset();
if (want_interactive) if (want_interactive)
yy_set_interactive(true); yy_set_interactive(1);
return 0; return 0;
} }

8
spot/tl/randomltl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire // Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016
// de Recherche et Développement de l'Epita (LRDE). // Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
@ -412,9 +412,9 @@ namespace spot
opt_seed_ = opts.get("seed", 0); opt_seed_ = opts.get("seed", 0);
opt_tree_size_min_ = opts.get("tree_size_min", 15); opt_tree_size_min_ = opts.get("tree_size_min", 15);
opt_tree_size_max_ = opts.get("tree_size_max", 15); opt_tree_size_max_ = opts.get("tree_size_max", 15);
opt_unique_ = opts.get("unique", true);
opt_wf_ = opts.get("wf", false);
opt_simpl_level_ = opts.get("simplification_level", 3); opt_simpl_level_ = opts.get("simplification_level", 3);
opt_unique_ = opts.get("unique", 1);
opt_wf_ = opts.get("wf", 0);
const char* tok_pL = nullptr; const char* tok_pL = nullptr;
const char* tok_pS = nullptr; const char* tok_pS = nullptr;

4
spot/twa/acc.cc
View file

@ -299,7 +299,7 @@ namespace spot
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();
} }
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();
return false; return 0U;
} }
} }
@ -532,7 +532,7 @@ namespace spot
if (max) if (max)
res = odd ? t() : f(); res = odd ? t() : f();
else else
res = (sets & 1) == odd ? t() : f(); res = ((sets & 1) == odd) ? t() : f();
if (sets == 0) if (sets == 0)
return res; return res;

6
spot/twaalgos/postproc.hh
View file

@ -1,6 +1,6 @@
// -*- 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.
// //
@ -178,7 +178,7 @@ namespace spot
// Fine-tuning options fetched from the option_map. // Fine-tuning options fetched from the option_map.
bool degen_reset_ = true; bool degen_reset_ = true;
bool degen_order_ = false; bool degen_order_ = false;
int degen_cache_ = true; int degen_cache_ = 1;
bool degen_lskip_ = true; bool degen_lskip_ = true;
bool degen_lowinit_ = false; bool degen_lowinit_ = false;
bool det_scc_ = true; bool det_scc_ = true;