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

fix some code smells reported by sonarcloud

Browse source 
* bench/dtgbasat/gen.py, bin/autcross.cc, bin/autfilt.cc,
bin/common_aoutput.cc, bin/common_aoutput.hh: Various cleanups.
This commit is contained in:
Alexandre Duret-Lutz 2023-01-05 23:34:10 +01:00
parent 36e79ecca6
commit 4a78d1bff4
5 changed files with 51 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

6
bench/dtgbasat/gen.py
View file

@ -1,5 +1,5 @@
#!/usr/bin/env python3
# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de
# Copyright (C) 2016-2018, 2023 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -55,12 +55,12 @@ class BenchConfig(object):
if line[0] == '#' or line.isspace():
continue
elif line[0:2] == "sh":
sh = re.search('sh (.+?)$', line).group(1)
sh = re.search('sh (.+)$', line).group(1)
continue
else:
name = re.search('(.+?):', line).group(1)
code = re.search(':(.+?)>', line).group(1)
xoptions = re.search('>(.+?)$', line).group(1)
xoptions = re.search('>(.+)$', line).group(1)
b = Bench(name=name, code=code, xoptions=xoptions)
self.l.append(b)
self.sh.append(sh)

12
bin/autcross.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et
// Copyright (C) 2017-2020, 2022-2023 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -549,7 +549,7 @@ namespace
{
if (!quiet)
std::cerr << "info: building " << autname(i, is_really_comp(i))
<< '*' << autname(j, true ^ is_really_comp(j))
<< '*' << autname(j, !is_really_comp(j))
<< " requires more acceptance sets than supported\n";
return false;
}
@ -557,14 +557,14 @@ namespace
if (verbose)
std::cerr << "info: check_empty "
<< autname(i, is_really_comp(i))
<< '*' << autname(j, true ^ is_really_comp(j)) << '\n';
<< '*' << autname(j, !is_really_comp(j)) << '\n';
auto w = aut_i->intersecting_word(aut_j);
if (w)
{
std::ostream& err = global_error();
err << "error: " << autname(i, is_really_comp(i))
<< '*' << autname(j, true ^ is_really_comp(j))
<< '*' << autname(j, !is_really_comp(j))
<< (" is nonempty; both automata accept the infinite word:\n"
" ");
example() << *w << '\n';
@ -613,7 +613,7 @@ namespace
return src.str();
}();
input_statistics.push_back(in_statistics());
input_statistics.emplace_back(in_statistics());
input_statistics[round_num].input_source = std::move(source);
if (auto name = input->get_named_prop<std::string>("automaton-name"))
@ -658,7 +658,7 @@ namespace
problems += prob;
}
spot::cleanup_tmpfiles();
output_statistics.push_back(std::move(stats));
output_statistics.emplace_back(std::move(stats));
if (verbose)
{

79
bin/autfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -448,7 +448,7 @@ struct canon_aut
std::vector<tr_t> edges;
std::string acc;
canon_aut(const spot::const_twa_graph_ptr& aut)
explicit canon_aut(const spot::const_twa_graph_ptr& aut)
: num_states(aut->num_states())
, edges(aut->edge_vector().begin() + 1,
aut->edge_vector().end())
@ -755,6 +755,22 @@ product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
return spot::product_or(left, right);
}
static spot::twa_graph_ptr
word_to_aut(const char* word, const char *argname)
{
try
{
return spot::parse_word(word, opt->dict)->as_automaton();
}
catch (const spot::parse_error& e)
{
error(2, 0, "failed to parse the argument of --%s:\n%s",
argname, e.what());
}
SPOT_UNREACHABLE();
return nullptr;
}
static int
parse_opt(int key, char* arg, struct argp_state*)
{
@ -776,17 +792,14 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case 'u':
opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
opt->uniq = std::make_unique<unique_aut_t>();
break;
case 'v':
opt_invert = true;
break;
case 'x':
{
const char* opt = extra_options.parse_options(arg);
if (opt)
error(2, 0, "failed to parse --options near '%s'", opt);
}
if (const char* opt = extra_options.parse_options(arg))
error(2, 0, "failed to parse --options near '%s'", opt);
break;
case OPT_ALIASES:
opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types);
@ -802,16 +815,7 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_art_sccs_set = true;
break;
case OPT_ACCEPT_WORD:
try
{
opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
->as_automaton());
}
catch (const spot::parse_error& e)
{
error(2, 0, "failed to parse the argument of --accept-word:\n%s",
e.what());
}
opt->acc_words.emplace_back(word_to_aut(arg, "accept-word"));
break;
case OPT_ACCEPTANCE_IS:
{
@ -964,16 +968,7 @@ parse_opt(int key, char* arg, struct argp_state*)
"%d should be followed by a comma and WORD", res);
arg = endptr + 1;
}
try
{
opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
->as_automaton(), res);
}
catch (const spot::parse_error& e)
{
error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
e.what());
}
opt->hl_words.emplace_back(word_to_aut(arg, "highlight-word"), res);
}
break;
case OPT_HIGHLIGHT_LANGUAGES:
@ -1157,16 +1152,7 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_art_sccs_set = true;
break;
case OPT_REJECT_WORD:
try
{
opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
->as_automaton());
}
catch (const spot::parse_error& e)
{
error(2, 0, "failed to parse the argument of --reject-word:\n%s",
e.what());
}
opt->rej_words.emplace_back(word_to_aut(arg, "reject-word"));
break;
case OPT_REM_AP:
opt->rem_ap.add_ap(arg);
@ -1291,7 +1277,7 @@ namespace
static
bool match_acceptance(spot::twa_graph_ptr aut)
{
auto& acc = aut->acc();
const spot::acc_cond& acc = aut->acc();
switch (opt_acceptance_is)
{
case ACC_Any:
@ -1346,8 +1332,7 @@ namespace
{
bool max;
bool odd;
bool is_p = acc.is_parity(max, odd, true);
if (!is_p)
if (!acc.is_parity(max, odd, true))
return false;
switch (opt_acceptance_is)
{
@ -1460,7 +1445,7 @@ namespace
if (matched && opt_acceptance_is)
matched = match_acceptance(aut);
if (matched && (opt_sccs_set | opt_art_sccs_set))
if (matched && (opt_sccs_set || opt_art_sccs_set))
{
spot::scc_info si(aut);
unsigned n = si.scc_count();
@ -1540,14 +1525,14 @@ namespace
&& spot::contains(aut, opt->equivalent_pos);
if (matched && !opt->acc_words.empty())
for (auto& word_aut: opt->acc_words)
for (const spot::twa_graph_ptr& word_aut: opt->acc_words)
if (spot::product(aut, word_aut)->is_empty())
{
matched = false;
break;
}
if (matched && !opt->rej_words.empty())
for (auto& word_aut: opt->rej_words)
for (const spot::twa_graph_ptr& word_aut: opt->rej_words)
if (!spot::product(aut, word_aut)->is_empty())
{
matched = false;
@ -1681,13 +1666,13 @@ namespace
aut->accepting_run()->highlight(opt_highlight_accepting_run);
if (!opt->hl_words.empty())
for (auto& word_aut: opt->hl_words)
for (auto& [word_aut, color]: opt->hl_words)
{
if (aut->acc().uses_fin_acceptance())
error(2, 0,
"--highlight-word does not yet work with Fin acceptance");
if (auto run = spot::product(aut, word_aut.first)->accepting_run())
run->project(aut)->highlight(word_aut.second);
if (auto run = spot::product(aut, word_aut)->accepting_run())
run->project(aut)->highlight(color);
}
timer.stop();

12
bin/common_aoutput.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
const spot::const_twa_graph_ptr& aut,
spot::formula f,
const char* filename, int loc,
spot::process_timer& ptimer,
const spot::process_timer& ptimer,
const char* csv_prefix, const char* csv_suffix)
{
timer_ = ptimer;
@ -633,10 +633,10 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
outputnamer.print(haut, aut, f, filename, loc, ptimer,
csv_prefix, csv_suffix);
std::string fname = outputname.str();
auto p = outputfiles.emplace(fname, nullptr);
if (p.second)
p.first->second.reset(new output_file(fname.c_str()));
out = &p.first->second->ostream();
auto [it, b] = outputfiles.try_emplace(fname, nullptr);
if (b)
it->second.reset(new output_file(fname.c_str()));
out = &it->second->ostream();
}
// Output it.

8
bin/common_aoutput.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2014-2018, 2020, 2022, 2023 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -155,7 +155,7 @@ public:
print(const spot::const_parsed_aut_ptr& haut,
const spot::const_twa_graph_ptr& aut,
spot::formula f,
const char* filename, int loc, spot::process_timer& ptimer,
const char* filename, int loc, const spot::process_timer& ptimer,
const char* csv_prefix, const char* csv_suffix);
private:
@ -196,7 +196,7 @@ class automaton_printer
std::map<std::string, std::unique_ptr<output_file>> outputfiles;
public:
automaton_printer(stat_style input = no_input);
explicit automaton_printer(stat_style input = no_input);
~automaton_printer();
void