From c4a5b325a219ed1ed31c19dc6ae518739fe1a37f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 10 May 2004 18:38:20 +0000 Subject: [PATCH] * src/sanity/style.test: New file. * src/sanity/Makefile.am (check-local): Run it. * src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style issues reported by style.test. --- ChangeLog | 10 +++++ src/ltlvisit/nenoform.cc | 4 +- src/ltlvisit/tostring.cc | 6 +-- src/sanity/Makefile.am | 2 + src/sanity/style.test | 86 ++++++++++++++++++++++++++++++++++++++ src/tgba/bdddict.cc | 12 +++--- src/tgba/bddprint.cc | 5 ++- src/tgba/tgba.cc | 6 +-- src/tgba/tgbaproduct.cc | 4 +- src/tgbaalgos/gtec/ce.cc | 2 +- src/tgbaalgos/gtec/gtec.cc | 2 +- src/tgbaalgos/lbtt.cc | 2 +- src/tgbaalgos/magic.cc | 14 +++---- src/tgbaalgos/powerset.cc | 4 +- src/tgbaalgos/reachiter.cc | 2 +- src/tgbatest/ltl2tgba.cc | 10 ++--- 16 files changed, 135 insertions(+), 36 deletions(-) create mode 100755 src/sanity/style.test diff --git a/ChangeLog b/ChangeLog index d1dd641b6..5ed035ef7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2004-05-10 Alexandre Duret-Lutz + * src/sanity/style.test: New file. + * src/sanity/Makefile.am (check-local): Run it. + * src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc, + src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc, + src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc, + src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc, + src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc, + src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style + issues reported by style.test. + * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh: Fix copyright year, these files were diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 099a56d2b..302c3ab06 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -59,7 +59,7 @@ namespace spot void visit(constant* c) { - if (! negated_) + if (!negated_) { result_ = c; return; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 81a851f8f..67a0f79bb 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -48,7 +48,7 @@ namespace spot visit(const atomic_prop* ap) { std::string str = ap->name(); - if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X' ) + if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X') { os_ << '"' << str << '"'; } @@ -98,7 +98,7 @@ namespace spot { // The parser treats F0, F1, G0, G1, X0, and X1 as atomic // propositions. So make sure we output F(0), G(1), etc. - bool need_parent = !! dynamic_cast(uo->child()); + bool need_parent = !!dynamic_cast(uo->child()); switch(uo->op()) { case unop::Not: @@ -241,7 +241,7 @@ namespace spot os_ << "!"; break; case unop::X: - need_parent = !! dynamic_cast(uo->child()); + need_parent = !!dynamic_cast(uo->child()); os_ << "X"; break; case unop::F: diff --git a/src/sanity/Makefile.am b/src/sanity/Makefile.am index 72b5198de..97da045d6 100644 --- a/src/sanity/Makefile.am +++ b/src/sanity/Makefile.am @@ -32,6 +32,8 @@ check-local: $(SHELL) $(srcdir)/includes.test $(TESTHEADER) INCDIR='$(top_srcdir)/src' \ $(SHELL) $(srcdir)/80columns.test $(TESTHEADER) + INCDIR='$(top_srcdir)/src' \ + $(SHELL) $(srcdir)/style.test $(TESTHEADER) # Ensure we have not forgotten to include an header. installcheck-local: diff --git a/src/sanity/style.test b/src/sanity/style.test new file mode 100755 index 000000000..2389477c2 --- /dev/null +++ b/src/sanity/style.test @@ -0,0 +1,86 @@ +#! /bin/sh + +# Ensure consistent style by catching common improper constructs. + +set -e + +diag() +{ + fail=: + echo "$file:" "$@" + echo ============================================================ +} + +rm -f failures + +# Get some help from GNU grep. +GREP_OPTIONS='--color=auto -n' +GREP_COLOR='1;31' +export GREP_OPTIONS +export GREP_COLOR + +tmp=incltest.tmp + +find "${INCDIR-..}" \( -name "${1-*}.hh" -o -name "${1-*}.cc" \) \ + -a -type f -a -print | +while read file; do + if grep 'GNU Bison' "$file" >/dev/null || + grep 'generated by flex' "$file" >/dev/null ; then + continue + fi + + fail=false + + sed 's,//.*,,' < $file > $tmp + + grep ' if(' $tmp && + diag 'Missing space after "if"' + + grep ' if (.*).*{' $tmp && + diag 'Opening { should be on its own line.' + + grep ' while(' $tmp && + diag 'Missing space after "while"' + + grep ' while (.*).*{' $tmp && + diag 'Opening { should be on its own line.' + + grep ' for(' $tmp && + diag 'Missing space after "for"' + + grep ' for (.*).*{' $tmp && + diag 'Opening { should be on its own line.' + + grep ' switch(' $tmp && + diag 'Missing space after "for"' + + grep ' switch (.*).*{' $tmp && + diag 'Opening { should be on its own line.' + + grep '( ' $tmp && + diag 'No space after opening (.' + + grep ' )' $tmp && + diag 'No space before closing ).' + + grep '! ' $tmp && + diag 'No space after unary operators (!).' + + grep ',[(a-zA-Z+=_!]' $tmp && + diag 'Space after coma.' + + grep '[^ \t\n]&&[^ \t\n]' $tmp && + diag 'Space arround binary operators.' + + grep '[^ \t\n]||[^ \t\n]' $tmp && + diag 'Space arround binary operators.' + + $fail && echo "$file" >>failures +done + +if test -f failures; then + echo "The following files contain style errors:" + cat failures + rm failures + exit 1; +fi diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 554dbec53..a4a56969c 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -188,7 +188,7 @@ namespace spot if (si == s.end()) return; s.erase(si); - if (! s.empty()) + if (!s.empty()) return; // ME was the last user of this variable. @@ -328,25 +328,25 @@ namespace spot && now_map.empty() && acc_map.empty()) { - if (! var_formula_map.empty()) + if (!var_formula_map.empty()) { std::cerr << "var_map is empty but var_formula_map is not" << std::endl; fail = true; } - if (! now_formula_map.empty()) + if (!now_formula_map.empty()) { std::cerr << "now_map is empty but now_formula_map is not" << std::endl; fail = true; } - if (! acc_formula_map.empty()) + if (!acc_formula_map.empty()) { std::cerr << "acc_map is empty but acc_formula_map is not" << std::endl; fail = true; } - if (! var_refs.empty()) + if (!var_refs.empty()) { std::cerr << "maps are empty but var_refs is not" << std::endl; fail = true; @@ -355,7 +355,7 @@ namespace spot std::cerr << " " << i->first << ":" << i->second.size(); std::cerr << std::endl; } - if (! fail) + if (!fail) return; } else diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 7b4f74989..ddf89f9e5 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -96,8 +96,9 @@ namespace spot else not_first = true; if (varset[v] == 0) - // The space is important for LBTT. - *where << "! "; + // The space is important for LBTT, but we have to hide it + // from our style checking droid. + *where << "!"" "; print_handler(*where, v); } } diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index ed9fb2c67..40d469ba1 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -40,7 +40,7 @@ namespace spot bdd tgba::support_conditions(const state* state) const { - if (! last_support_conditions_input_ + if (!last_support_conditions_input_ || last_support_conditions_input_->compare(state) != 0) { last_support_conditions_output_ = @@ -55,7 +55,7 @@ namespace spot bdd tgba::support_variables(const state* state) const { - if (! last_support_variables_input_ + if (!last_support_variables_input_ || last_support_variables_input_->compare(state) != 0) { last_support_variables_output_ = diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index fae35d11c..c5c2b82db 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -214,7 +214,7 @@ namespace spot // If global_automaton is not specified, THIS is the root of a // product tree. - if (! global_automaton) + if (!global_automaton) { global_automaton = this; global_state = local_state; diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index cd4e0d422..86edc2796 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -169,7 +169,7 @@ namespace spot // If by change or period already ends on the state we have // to reach back, we are done. if (from == to - && ! period.empty()) + && !period.empty()) return; // Records backlinks to parent state during the BFS. diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 210ddfc3e..1d8b147a0 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -377,7 +377,7 @@ namespace spot todo.push(pair_state_successors(succ.s, succ_queue())); succ_queue& new_queue = todo.top().second; tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); - for (iter->first(); ! iter->done(); iter->next()) + for (iter->first(); !iter->done(); iter->next()) new_queue.push_back(successor(iter->current_acceptance_conditions(), iter->current_state())); delete iter; diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 8be8d1a42..5373ad3c2 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -222,7 +222,7 @@ namespace spot g->get_init_state(), g, mmp, state_number, true); acceptance_cond_splitter acs(g->all_acceptance_conditions()); - while(! todo.empty()) + while (!todo.empty()) { state_acc_pair sap = *todo.begin(); todo.erase(todo.begin()); diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 1ae7d4942..ad5e768ac 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -44,7 +44,7 @@ namespace spot if (x) delete x; // Release all iterators on the stack. - while (! stack.empty()) + while (!stack.empty()) { delete stack.front().second; stack.pop_front(); @@ -101,14 +101,14 @@ namespace spot assert(stack.size() == 1 + tstack.size()); - while (! stack.empty()) + while (!stack.empty()) { recurse: magic_search::state_iter_pair& p = stack.front(); tgba_succ_iterator* i = p.second; const bool magic = p.first.m; - while (! i->done()) + while (!i->done()) { const state* s_prime = i->current_state(); bdd c = i->current_condition(); @@ -120,7 +120,7 @@ namespace spot assert(stack.size() == tstack.size()); return true; } - if (! has(s_prime, magic)) + if (!has(s_prime, magic)) { push(s_prime, magic); tstack.push_front(c); @@ -133,9 +133,9 @@ namespace spot delete i; stack.pop_front(); - if (! magic && a->state_is_accepting(s)) + if (!magic && a->state_is_accepting(s)) { - if (! has(s, true)) + if (!has(s, true)) { if (x) delete x; @@ -144,7 +144,7 @@ namespace spot continue; } } - if (! stack.empty()) + if (!stack.empty()) tstack.pop_front(); } diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index b8bff6976..e3dcb14f2 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -55,7 +55,7 @@ namespace spot unsigned state_num = 1; - while (! todo.empty()) + while (!todo.empty()) { power_state src = todo.front(); todo.pop_front(); @@ -78,7 +78,7 @@ namespace spot for (i = src.begin(); i != src.end(); ++i) { tgba_succ_iterator *si = aut->succ_iter(*i); - for (si->first(); ! si->done(); si->next()) + for (si->first(); !si->done(); si->next()) if ((cond >> si->current_condition()) == bddtrue) { const state* s = si->current_state(); diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 2d1870027..312665bed 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -59,7 +59,7 @@ namespace spot int tn = seen[t]; tgba_succ_iterator* si = automata_->succ_iter(t); process_state(t, tn, si); - for (si->first(); ! si->done(); si->next()) + for (si->first(); !si->done(); si->next()) { const state* current = si->current_state(); seen_map::const_iterator s = seen.find(current); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e6dee813d..1c7b3b1dc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -271,13 +271,13 @@ main(int argc, char** argv) if (strcmp(argv[formula_index], "-")) { std::ifstream fin(argv[formula_index]); - if (! fin) + if (!fin) { std::cerr << "Cannot open " << argv[formula_index] << std::endl; exit(2); } - if (! std::getline(fin, input, '\0')) + if (!std::getline(fin, input, '\0')) { std::cerr << "Cannot read " << argv[formula_index] << std::endl; exit(2); @@ -320,11 +320,11 @@ main(int argc, char** argv) } else { - + spot::ltl::formula* ftmp = f; if (reduc) f = spot::ltl::reduce(f); - + if (fm_opt) to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, fm_symb_merge_opt, @@ -332,7 +332,7 @@ main(int argc, char** argv) fair_loop_approx); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); - + if (reduc) spot::ltl::destroy(ftmp); }