* 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

@@ -1,5 +1,15 @@
 2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* 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

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;

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<const constant*>(uo->child());
+	bool need_parent = !!dynamic_cast<const constant*>(uo->child());
 	switch(uo->op())
 	  {
 	  case unop::Not:
@@ -241,7 +241,7 @@ namespace spot
 	    os_ << "!";
 	    break;
 	  case unop::X:
-	    need_parent = !! dynamic_cast<const constant*>(uo->child());
+	    need_parent = !!dynamic_cast<const constant*>(uo->child());
 	    os_ << "X";
 	    break;
 	  case unop::F:

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:

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

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

src/tgba/bddprint.cc

@@ -96,8 +96,9 @@ namespace spot
 	else
 	  not_first = true;
 	if (varset[v] == 0)
-	  // The space is important for LBTT.
+	  // The space is important for LBTT, but we have to hide it
-	  *where << "! ";
+	  // from our style checking droid.
+	  *where << "!"" ";
 	print_handler(*where, v);
       }
   }

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_ =

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;

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.

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;

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());

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();
       }
 

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();

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);

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);