99241d0bea
* ChangeLog.1, tests/core/autcross3.test, tests/core/ltl3ba.test, tests/core/ltl3dra.test, tests/core/ltlcross3.test, tests/core/ltlsynt.test, tests/sanity/style.test: Here.
397 lines
12 KiB
Bash
Executable file
397 lines
12 KiB
Bash
Executable file
#! /bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de
|
|
# l'Epita (LRDE).
|
|
# Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
|
|
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
|
|
# Pierre et Marie Curie.
|
|
#
|
|
# This file is part of Spot, a model checking library.
|
|
#
|
|
# Spot is free software; you can redistribute it and/or modify it
|
|
# under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation; either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
# License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
# Ensure consistent style by catching common improper constructs.
|
|
|
|
set -e
|
|
set +x
|
|
|
|
diag()
|
|
{
|
|
fail=:
|
|
echo "$file:" "$@"
|
|
echo ============================================================
|
|
}
|
|
|
|
rm -f failures.style
|
|
|
|
GREP=grep
|
|
|
|
# Get some help from GNU grep.
|
|
if (grep --color=auto -n --version)>/dev/null 2>&1; then
|
|
GREP="$GREP --color=auto -n"
|
|
GREP_COLOR='1;31'
|
|
export GREP_COLOR
|
|
fi
|
|
|
|
# Reset the locale, so for instance we don't get bugs because sed is
|
|
# expecting utf-8 and we feed it latin-1. The C locale should be OK,
|
|
# because we do not treat extended characters specifically in the
|
|
# following style rules.
|
|
LC_ALL=C
|
|
export LC_ALL
|
|
|
|
mkdir -p style.dir
|
|
tmp=style.dir/incltest.tmp.$$
|
|
|
|
# We used to loop over more directories before the source tree was
|
|
# rearranged. So there is only one left today, but we keep the loop
|
|
# in case we want to add more in the future.
|
|
TOP=${srcdir-.}/../..
|
|
for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do
|
|
|
|
find "$dir" \( -name "${1-*}.hh" \
|
|
-o -name "${1-*}.hxx" \
|
|
-o -name "${1-*}.cc" \
|
|
-o -name "${1-*}.test" \) \
|
|
-a -not -path '*.dir/*' \
|
|
-a -type f -a -print |
|
|
while read file; do
|
|
if $GREP 'GNU Bison' "$file" >/dev/null ||
|
|
$GREP '/robin-hood-hashing' "$file" >/dev/null ||
|
|
$GREP 'generated by flex' "$file" >/dev/null ; then
|
|
continue
|
|
fi
|
|
|
|
# Skip the files used by sanity.
|
|
case $file in
|
|
*incltest.cc) continue;;
|
|
esac
|
|
|
|
fail=false
|
|
|
|
# Check this before stripping comments and strings.
|
|
$GREP -i 'accepting cond' $file && diag 'accepting -> acceptance'
|
|
$GREP -i 'dictionnar[yi]' $file && diag 'dictionnary -> dictionary'
|
|
# "an uninstalled" seems to be the exception so far, but we want
|
|
# "a unique", "a universal", etc.
|
|
$GREP -i 'an uni[^n]' $file && diag 'an uni... -> a uni...'
|
|
|
|
$GREP -i 'version 2 of the License' $file &&
|
|
diag 'license text should refer to version 2'
|
|
$GREP -i 'Temple Place' $file &&
|
|
diag 'license text should give a url instead of an address'
|
|
|
|
$GREP -q 'coding: utf-8' $file ||
|
|
diag 'missing -*- coding: utf-8 -*-'
|
|
|
|
$GREP Copyright $file >/dev/null ||
|
|
diag "missing copyright"
|
|
|
|
# If some grep implementation ignores LC_ALL=C, this rule might be
|
|
# a problem on utf-8 characters such as "δ" which really
|
|
# corresponds to multiple bytes, but might be matched as a single
|
|
# character by grep.
|
|
$GREP '<< *"\([^\\]\|\\.\)"' $file &&
|
|
diag "Use << 'c' instead" 'of << "c".'
|
|
|
|
# A doxygen comments such as
|
|
#
|
|
# | \brief foo
|
|
# | \ingroup bar
|
|
# |
|
|
# | baz
|
|
#
|
|
# will be output as "foobaz." But if the first two lines
|
|
# are reversed, it's output correctly.
|
|
perl -ne '/(.*\\brief.*\n.*\\ingroup.*)/ && print("$1\n") && exit(1)' \
|
|
-0777 $file || diag "always put 'ingroup' before 'brief'"
|
|
|
|
# Check this before we remove SPOT_API from the input.
|
|
case $file in
|
|
*.cc)
|
|
$GREP 'SPOT_API' $file &&
|
|
diag 'use SPOT_API only in header files';;
|
|
esac
|
|
|
|
# Strip comments and strings.
|
|
#
|
|
# Multi-line comments of the form
|
|
# /* Line 1
|
|
# Line 2
|
|
# Line 3 */
|
|
# are replaced by
|
|
# //
|
|
# //
|
|
# //
|
|
# to keep the line numbers correct in the diagnostics.
|
|
#
|
|
# Also get rid of the SPOT_API tags.
|
|
perl -pe 'sub f {my $a = shift; $a =~ s:[^\n]*://:g; return "$a"}
|
|
s,/\*(.*?)\*/,f($1),sge;
|
|
s,//.*?\n,//\n,g;
|
|
s,(?<!include )"(\\.|[^"\\\n])*","",g;
|
|
s,SPOT_API ,,g' -0777 <$file >$tmp
|
|
|
|
$GREP '[ ]$' $tmp &&
|
|
diag 'Trailing whitespace.'
|
|
|
|
case $file in
|
|
*.test);;
|
|
*)
|
|
$GREP -E '(>[^>]*|^[^<]*)class[ \t]+[A-Z]' $tmp &&
|
|
diag 'Use lower case class names.'
|
|
|
|
$GREP '[ ]if(' $tmp &&
|
|
diag 'Missing space after "if"'
|
|
|
|
$GREP '[ ]if ([^()]*).*{' $tmp &&
|
|
diag 'Opening { should be on its own line.'
|
|
|
|
$GREP '[ ]if ([^()]*).*;' $tmp &&
|
|
diag 'if body should be on another line.'
|
|
|
|
$GREP '[ ]if ([^()]*([^()]*)[^()]*).*;' $tmp &&
|
|
diag 'if body should be on another line.'
|
|
|
|
$GREP '[ ]else.*;' $tmp &&
|
|
diag 'else body should be on another line.'
|
|
|
|
$GREP '[ ]while(' $tmp &&
|
|
diag 'Missing space after "while"'
|
|
|
|
$GREP '[ ]while (.*).*{' $tmp &&
|
|
diag 'Opening { should be on its own line.'
|
|
|
|
$GREP '[ ]while (.*).*[^)];' $tmp &&
|
|
diag 'while body should be on another line.'
|
|
|
|
$GREP '[ ]for(' $tmp &&
|
|
diag 'Missing space after "for"'
|
|
|
|
$GREP '[ ]for (.*).*{' $tmp &&
|
|
diag 'Opening { should be on its own line.'
|
|
|
|
$GREP '[ ]for (.*;.*;.*).*;' $tmp &&
|
|
diag 'for body should be on another line.'
|
|
|
|
$GREP '[ ]switch(' $tmp &&
|
|
diag 'Missing space after "switch"'
|
|
|
|
$GREP '[ ]switch (.*).*{' $tmp &&
|
|
diag 'Opening { should be on its own line.'
|
|
|
|
$GREP 'namespace .*{' $tmp &&
|
|
diag 'Opening { should be on its own line.'
|
|
|
|
$GREP 'class .*{' $tmp | $GREP -v enum &&
|
|
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 ",[^ \" %'\\\\]" $tmp &&
|
|
diag 'Space after comma.'
|
|
|
|
# The 'r' allows operator&&
|
|
# The '.' allows &&...
|
|
# The ')' allows foo(bar&&)
|
|
$GREP '[^ r]&&[^ .)]' $tmp &&
|
|
diag 'Space around binary operators.'
|
|
|
|
# The 'r' allows operator||
|
|
$GREP '[^ r]||[^ ]' $tmp &&
|
|
diag 'Space around binary operators.'
|
|
|
|
# The 'r' allows operator==
|
|
$GREP '[^ r<>][!<>=]=[^ ]' $tmp &&
|
|
diag 'Space around binary operators.'
|
|
|
|
# The 'r' allows operator<<=
|
|
$GREP '[^ r][<>][<>]=[^ ]' $tmp &&
|
|
diag 'Space around binary operators.'
|
|
|
|
$GREP 'operator[^a-zA-Z0-9_(]*[ ][^a-zA-Z0-9_(]*(' $tmp &&
|
|
diag 'Write operatorXX(...) without spaces around XX.'
|
|
|
|
$GREP 'operator[^(]* (' $tmp &&
|
|
diag 'No space before ('
|
|
|
|
$GREP '[ ]default:[^:].*;' $tmp &&
|
|
diag 'Label should be on their own line.'
|
|
|
|
$GREP '[ ]case.*:[^:].*;' $tmp &&
|
|
diag 'Label should be on their own line.'
|
|
|
|
$GREP '[ ];' $tmp &&
|
|
diag 'No space before semicolon.'
|
|
|
|
$GREP -v 'for (.*;;)' $tmp | $GREP ';[^ ")'"']" &&
|
|
diag 'Must have space or newline after semicolon.'
|
|
|
|
# Allow several { or } on the same line only if they are mixed
|
|
# with parentheses, as this often occur with lambdas or
|
|
# initializer lists. What we want to forbid is cases where
|
|
# multiple scopes are opened/closed on the same line.
|
|
$GREP '^[^():]*}[^()]*}[^()]*$' $tmp &&
|
|
diag 'No two } on the same line.'
|
|
|
|
$GREP '^[^()]{[^()]*{[^()]$' $tmp &&
|
|
diag 'No two { on the same line.'
|
|
|
|
$GREP 'delete[ ]*[(][^(]*[)];' $tmp |
|
|
$GREP -v 'operator[ ]*delete[ ]*[(][^(]*[)];' &&
|
|
diag 'No useless parentheses after delete.'
|
|
|
|
$GREP 'return[ ]*[(][^(]*[)];' $tmp &&
|
|
diag 'No useless parentheses after return.'
|
|
|
|
$GREP 'NULL' $tmp &&
|
|
diag 'Use nullptr instead of NULL.'
|
|
|
|
# std::list::size() can be O(n). Better use empty() whenever
|
|
# possible, even for other containers.
|
|
e$GREP '(->|[.])size\(\) [=!]= 0|![a-zA-Z0-9_]*(->|[.])size\(\)|(if |while |assert)\([a-zA-Z0-9_]*(->|[.])size\(\)\)' $tmp &&
|
|
diag 'Prefer empty() to check emptiness.'
|
|
|
|
$GREP -E 'std::cerr.*<<.*endl' $tmp &&
|
|
diag 'std::cerr has unitbuf set; use \\n instead of endl'
|
|
|
|
e$GREP 'assert\((0|!".*")\)' $tmp &&
|
|
diag 'Prefer SPOT_UNREACHABLE or SPOT_UNIMPLEMENTED.'
|
|
|
|
e$GREP '^[^=*<]*([+][+]|--);' $tmp &&
|
|
diag 'Take good habits: use ++i instead of i++ when you have the choice.'
|
|
|
|
$GREP '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp &&
|
|
diag 'Use "x->y", not "(*x).y"'
|
|
|
|
# we allow these functions only in ?...:...
|
|
e$GREP 'bdd_(false|true)[ ]*\(' $tmp | $GREP -v '[?:]' &&
|
|
diag 'Use bddfalse and bddtrue instead of bdd_false() and bdd_true()'
|
|
|
|
res=`perl -ne '$/ = undef;
|
|
print "$&\n"
|
|
while /if \((.*)(\s*==\s*0)?\)\s*delete(\[\])?\s+\1;(?!\s+else)/g' $tmp`
|
|
if test -n "$res"; then
|
|
echo "$res"
|
|
diag 'No "if (x)" required before "delete x;".'
|
|
fi
|
|
|
|
# we want catch (const reftype&) or catch (...)
|
|
$GREP 'catch *([^.]' $tmp | $GREP -v 'const.*\&' &&
|
|
diag 'Always capture exceptions by const reference.'
|
|
|
|
case $file in
|
|
*.hh | *.hxx)
|
|
if e$GREP '(<<|>>)' $tmp >/dev/null; then
|
|
:
|
|
else
|
|
$GREP '#.*include.*<iostream>' $tmp &&
|
|
diag 'Avoid <iostream> in headers, better use <iosfwd>.'
|
|
fi
|
|
$GREP '^[ ]* ' $tmp &&
|
|
diag 'Use spaces instead of tabs.'
|
|
# Headers from spot/priv/ are not installed, so may only be
|
|
# included from *.cc files or from other spot/priv/ headers
|
|
# (in the latter case they do not have to specify the priv/
|
|
# directory, so they will not match this regex).
|
|
case $file in
|
|
*/priv/*|*/bin/*);;
|
|
*)
|
|
$GREP '#.*include.*priv/' $tmp &&
|
|
diag 'Do not include private headers in public headers.'
|
|
$GREP '^[^#]*[^#_]assert[ ]*(.*)' $tmp &&
|
|
diag 'Use SPOT_ASSERT() instead of assert() in public headers.'
|
|
;;
|
|
esac
|
|
case $file in
|
|
*/bin/*);;
|
|
*.hh)
|
|
$GREP '#.*include.*[<"]config.h[">]' $tmp &&
|
|
diag 'Do not include config.h in header files.'
|
|
esac
|
|
;;
|
|
*.cc)
|
|
if $GREP 'namespace$' $tmp >/dev/null; then
|
|
:
|
|
else
|
|
# We only check classes, but the rule should apply to functions too
|
|
$GREP '^[ ]*class[ ]' $tmp &&
|
|
diag 'Private definitions must be in anonymous namespace.'
|
|
fi
|
|
e$GREP ' ' $tmp &&
|
|
diag 'Use spaces instead of tabs.'
|
|
case $file in
|
|
*/bin/*) ;;
|
|
*)
|
|
if $GREP -q '#.*include.*"config.h"' $tmp; then
|
|
:
|
|
else
|
|
diag "*.cc files should include "'"config.h"'
|
|
fi;;
|
|
esac;;
|
|
esac
|
|
case $file in
|
|
*/bin/*|*.cc);;
|
|
*)
|
|
$GREP -v '#.*include.*priv/' $tmp | $GREP '#.*include.*"' &&
|
|
diag 'Use <header> instead of "header" for public headers.'
|
|
$GREP '#.*include.*<spot/priv/.*>' $tmp &&
|
|
diag 'Use "spot/priv/..." instead of <spot/priv/...>".'
|
|
;;
|
|
esac
|
|
;;
|
|
esac
|
|
|
|
|
|
$fail && echo "$file" >>failures.style
|
|
|
|
done || : # Make sure sh does not abort when read exits with false.
|
|
done
|
|
|
|
|
|
# Rules for Makefiles.
|
|
for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do
|
|
|
|
find "$dir" -name "Makefile.am" -a -type f -a -print |
|
|
while read file; do
|
|
fail=false
|
|
|
|
# Strip comments.
|
|
sed 's,#.*,,' < $file > $tmp
|
|
|
|
$GREP '[ ]$' $tmp &&
|
|
diag 'Trailing whitespace.'
|
|
|
|
$GREP '\.libs/' $tmp &&
|
|
diag "Don't reference files in .libs/, use Libtool instead."
|
|
|
|
$fail && echo "$file" >>failures.style
|
|
done || : # Make sure sh does not abort when read exits with false.
|
|
done
|
|
|
|
if test -f failures.style; then
|
|
echo "The following files contain style errors:"
|
|
cat failures.style
|
|
rm failures.style
|
|
exit 1;
|
|
fi
|
|
|
|
exit 0
|