From 279bfa00bd71e8e2cfe1295ce86132867800b2ba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Oct 2016 22:53:29 +0200 Subject: [PATCH] fix some implicit promotion from bool, as suggested by PVS-Studio For #192. * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll, spot/tl/randomltl.cc, spot/twa/acc.cc, spot/twaalgos/postproc.hh: Here. --- spot/parseaut/parseaut.yy | 4 ++-- spot/parseaut/scanaut.ll | 4 ++-- spot/tl/randomltl.cc | 8 ++++---- spot/twa/acc.cc | 4 ++-- spot/twaalgos/postproc.hh | 6 +++--- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 46be5e95d..12a7ec517 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -2067,9 +2067,9 @@ static void fix_initial_state(result_& r) // Multiple initial states. We might need to add a fake one, // unless one of the actual initial state has no incoming edge. auto& aut = r.h->aut; - std::vector has_incoming(aut->num_states(), 0); + std::vector has_incoming(aut->num_states(), 0); for (auto& t: aut->edges()) - has_incoming[t.dst] = true; + has_incoming[t.dst] = 1; bool found = false; unsigned init = 0; diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index efb9891be..2018b63a2 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -425,7 +425,7 @@ namespace spot YY_NEW_FILE; hoayyreset(); if (want_interactive) - yy_set_interactive(true); + yy_set_interactive(1); return 0; } @@ -461,7 +461,7 @@ namespace spot YY_NEW_FILE; hoayyreset(); if (want_interactive) - yy_set_interactive(true); + yy_set_interactive(1); return 0; } diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index 7ff96dd39..95947667a 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -412,9 +412,9 @@ namespace spot opt_seed_ = opts.get("seed", 0); opt_tree_size_min_ = opts.get("tree_size_min", 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_unique_ = opts.get("unique", 1); + opt_wf_ = opts.get("wf", 0); const char* tok_pL = nullptr; const char* tok_pS = nullptr; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 407711c14..8643be22e 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -299,7 +299,7 @@ namespace spot SPOT_UNREACHABLE(); } SPOT_UNREACHABLE(); - return false; + return 0U; } } @@ -532,7 +532,7 @@ namespace spot if (max) res = odd ? t() : f(); else - res = (sets & 1) == odd ? t() : f(); + res = ((sets & 1) == odd) ? t() : f(); if (sets == 0) return res; diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 4bef4016a..b9d1174eb 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -178,7 +178,7 @@ namespace spot // Fine-tuning options fetched from the option_map. bool degen_reset_ = true; bool degen_order_ = false; - int degen_cache_ = true; + int degen_cache_ = 1; bool degen_lskip_ = true; bool degen_lowinit_ = false; bool det_scc_ = true;