move the sanity tests in tests/sanity/
* spot/sanity/: Move ... * tests/sanity/: ... here. * spot/sanity/Makefile.am: Merge with... * tests/Makefile.am: ... this. * tests/run.in: Learn to run perl tests. * README, configure.ac, spot/Makefile.am: Adjust. * spot/tl/mark.hh: Add missing SPOT_API detected by fixed private.test. * spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Move... * spot/priv/weight.cc, spot/priv/weight.hh: ... here, as suggested by fixed private.test. * spot/twaalgos/tau03opt.cc, spot/twaalgos/Makefile.am, spot/priv/Makefile.am: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
6b881a2e38
commit
6e854b6d83
19 changed files with 79 additions and 139 deletions
|
|
@ -1,6 +1,6 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
## et Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire
|
||||
## de Recherche et Développement de l'Epita (LRDE).
|
||||
## 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.
|
||||
|
|
@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects
|
|||
# end, after building '.' (since the current directory contains
|
||||
# libspot.la needed by the tests)
|
||||
SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \
|
||||
parseaut parsetl . ltsmin sanity
|
||||
parseaut parsetl . ltsmin
|
||||
|
||||
lib_LTLIBRARIES = libspot.la
|
||||
libspot_la_SOURCES =
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
## Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
||||
## Développement de l'Epita (LRDE).
|
||||
##
|
||||
## This file is part of Spot, a model checking library.
|
||||
|
|
@ -20,14 +20,14 @@
|
|||
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
noinst_HEADERS = \
|
||||
accmap.hh \
|
||||
bddalloc.hh \
|
||||
freelist.hh \
|
||||
trim.hh
|
||||
|
||||
noinst_LTLIBRARIES = libpriv.la
|
||||
libpriv_la_SOURCES = \
|
||||
accmap.hh \
|
||||
bddalloc.cc \
|
||||
bddalloc.hh \
|
||||
freelist.cc \
|
||||
trim.cc
|
||||
freelist.hh \
|
||||
trim.cc \
|
||||
trim.hh \
|
||||
weight.cc \
|
||||
weight.hh
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement
|
||||
// de l'Epita.
|
||||
// Copyright (C) 2011, 2014, 2016 Laboratoire de Recherche et
|
||||
// Developpement de l'Epita.
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
|
|
@ -22,7 +22,7 @@
|
|||
|
||||
#include <cassert>
|
||||
#include <ostream>
|
||||
#include <spot/twaalgos/weight.hh>
|
||||
#include <spot/priv/weight.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
4
spot/sanity/.gitignore
vendored
4
spot/sanity/.gitignore
vendored
|
|
@ -1,4 +0,0 @@
|
|||
Makefile.in
|
||||
Makefile
|
||||
incltest.cc
|
||||
incltest.tmp
|
||||
|
|
@ -1,68 +0,0 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012 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/>.
|
||||
|
||||
# Check that all files use at most 80 columns.
|
||||
|
||||
set -e
|
||||
|
||||
rm -f failures
|
||||
|
||||
LANG=en_US.UTF-8
|
||||
export LANG
|
||||
|
||||
if [ "`echo '{r₁|r₂|r₃}' | wc -m`" != 11 ]; then
|
||||
LANG=C
|
||||
export LANG
|
||||
# The current locale does not grok unicode.
|
||||
# We still run this test, but only on lines that are purely ascii.
|
||||
x='[^ -~]' # This blank is a tab.
|
||||
else
|
||||
x='.'
|
||||
fi
|
||||
x="$x$x$x$x$x$x$x$x$x" # 9x
|
||||
x="$x$x$x$x$x$x$x$x$x" # 81x
|
||||
|
||||
for dir in "${INCDIR-..}"; do
|
||||
|
||||
find "$dir" \( -name "${1-*}.hh" \
|
||||
-o -name "${1-*}.hxx" \
|
||||
-o -name "${1-*}.cc" \
|
||||
-o -name "${1-*}.test" \) -a -type f -a -print |
|
||||
while read file; do
|
||||
if (expand $file | grep -q $x) 2>/dev/null; then
|
||||
if grep 'GNU Bison' "$file" >/dev/null ||
|
||||
grep 'generated by flex' "$file" >/dev/null ; then
|
||||
:
|
||||
else
|
||||
echo "$file" >>failures
|
||||
fi
|
||||
fi
|
||||
done
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
echo "The following files contain lines with more than 80 characters:"
|
||||
cat failures
|
||||
rm failures
|
||||
exit 1;
|
||||
fi
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
## Recherche et Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2004 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
# Run `make TESTHEADER=foo.hh check' if you want to check only one
|
||||
# header.
|
||||
check-80columns:
|
||||
INCDIR='$(top_srcdir)/spot' \
|
||||
$(SHELL) $(srcdir)/80columns.test $(TESTHEADER)
|
||||
|
||||
check-style:
|
||||
INCDIR='$(top_srcdir)/spot' \
|
||||
$(SHELL) $(srcdir)/style.test $(TESTHEADER)
|
||||
|
||||
check-readme:
|
||||
top_srcdir='$(top_srcdir)' \
|
||||
$(PERL) $(srcdir)/readme.test
|
||||
|
||||
check-ipynb:
|
||||
top_srcdir='$(top_srcdir)' \
|
||||
$(PERL) $(srcdir)/ipynb.test
|
||||
|
||||
check-includes:
|
||||
CXX='$(CXX)' \
|
||||
CPPFLAGS='$(AM_CPPFLAGS) $(CPPFLAGS) $(DEFS)' \
|
||||
CXXFLAGS='$(AM_CXXFLAGS) $(CXXFLAGS)' \
|
||||
INCDIR='$(top_srcdir)/spot' \
|
||||
TOPBUILD='$(top_builddir)' \
|
||||
$(SHELL) $(srcdir)/includes.test $(TESTHEADER)
|
||||
|
||||
.PHONY: check-80columns check-style check-readme check-includes check-ipynb
|
||||
check-local: check-80columns check-style check-readme check-includes check-ipynb
|
||||
|
||||
# Ensure we have not forgotten to include an header.
|
||||
check-installed-includes:
|
||||
CXX='$(CXX)' \
|
||||
CPPFLAGS='-I $(includedir) -I$(pkgincludedir) $(CPPFLAGS)' \
|
||||
CXXFLAGS='$(AM_CXXFLAGS) $(CXXFLAGS)' \
|
||||
INCDIR='$(pkgincludedir)' \
|
||||
$(SHELL) $(srcdir)/includes.test $(TESTHEADER)
|
||||
|
||||
# Any installed header should contain a SPOT_API tag somewhere.
|
||||
check-installed-private:
|
||||
INCDIR='$(pkgincludedir)' \
|
||||
SRCDIR='$(top_srcdir)/src' \
|
||||
$(SHELL) $(srcdir)/private.test $(TESTHEADER)
|
||||
|
||||
|
||||
installcheck-local: check-installed-includes check-installed-private
|
||||
|
||||
CLEANFILES = failures incltest.*
|
||||
EXTRA_DIST = \
|
||||
80columns.test \
|
||||
includes.test \
|
||||
ipynb.test \
|
||||
private.test \
|
||||
readme.test \
|
||||
style.test
|
||||
|
|
@ -1,59 +0,0 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2008, 2011, 2012 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/>.
|
||||
|
||||
# Check that each header is self contained and generates no warning.
|
||||
|
||||
set -e
|
||||
|
||||
rm -f failures
|
||||
|
||||
# Remove any trailing slash
|
||||
INCDIR=${INCDIR%/}
|
||||
|
||||
for file in `find "$INCDIR" \( -name "${1-*}.hh" \
|
||||
-o -name "${1-*}.hxx" \) \
|
||||
-a -type f -a -print | sed "s,$INCDIR/,,g"`; do
|
||||
|
||||
if head -n 100 "$INCDIR/$file" | grep -q "[ ]*#.*pragma.* once\$"; then
|
||||
:
|
||||
elif grep -q 'GNU Bison 2\.6' "$INCDIR/$file"; then
|
||||
# Bison 2.6, 2.6.1, 2.6.2 have a bug where position.hh
|
||||
# include <iosfwd> instead of <iostream>.
|
||||
continue
|
||||
elif grep -q 'GNU Bison' "$INCDIR/$file"; then
|
||||
:
|
||||
else
|
||||
echo "Missing, or incorrect include guard." >&2
|
||||
echo "FAIL: $file"
|
||||
echo " $file" >> failures
|
||||
continue
|
||||
fi
|
||||
echo "PASS: $file"
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
echo "Failed files:"
|
||||
cat failures
|
||||
rm failures
|
||||
exit 1;
|
||||
fi
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
#! /usr/bin/perl -w
|
||||
# -*- cperl; coding: utf-8 -*-
|
||||
#
|
||||
# Copyright (C) 2010, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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/>.
|
||||
#
|
||||
# Check that all the directories documented in README exist, and that
|
||||
# all directories listed in configure.ac are documented.
|
||||
#
|
||||
# Also has an option --list to print directories which are
|
||||
# documented.
|
||||
|
||||
use strict;
|
||||
use warnings;
|
||||
|
||||
local $\ = "\n";
|
||||
my $top_srcdir = $ENV{top_srcdir} || "../../";
|
||||
my $top_srcdir_len = length($top_srcdir) + 1;
|
||||
|
||||
my $tut = "$top_srcdir/doc/org/tut.org";
|
||||
my $dir = "$top_srcdir/tests/python";
|
||||
unless (-f $tut)
|
||||
{
|
||||
print STDERR "$tut not found";
|
||||
exit 2;
|
||||
}
|
||||
|
||||
open(FD, "$tut") or die "$!: cannot open $tut";
|
||||
my $exit_status = 0;
|
||||
my %seen;
|
||||
while (<FD>)
|
||||
{
|
||||
if (m:\]\[=([\w-]+\.ipynb)=\]\]:)
|
||||
{
|
||||
# print "$1 documented";
|
||||
$seen{$1} = 1;
|
||||
unless (-f "$dir/$1")
|
||||
{
|
||||
print STDERR "notebook mentioned in tut.org does not exist";
|
||||
$exit_status = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
close(FD);
|
||||
|
||||
open(FD, "$dir/../Makefile.am") or die "$!";
|
||||
while (<FD>)
|
||||
{
|
||||
if (m:python/([\w-]+\.ipynb):)
|
||||
{
|
||||
# print "$1 exist";
|
||||
unless (exists $seen{$1})
|
||||
{
|
||||
print STDERR "notebook $1 is not mentioned in tut.org";
|
||||
$exit_status = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
close(FD);
|
||||
|
||||
exit $exit_status;
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
# Make sure we do not install privated header, i.e., headers that
|
||||
# declare unexported functions. We catch these by checking for
|
||||
# headers that have no SPOT_API occurrence, but that have an ssociated
|
||||
# *.cc file.
|
||||
|
||||
set -e
|
||||
|
||||
rm -f failures
|
||||
|
||||
# Remove any trailing slash
|
||||
INCDIR=${INCDIR%/}
|
||||
|
||||
for file in `find "$INCDIR" \( -name "${1-*}.hh" \
|
||||
-o -name "${1-*}.hxx" \) \
|
||||
-a -type f -a -print | sed "s,$INCDIR/,,g"`; do
|
||||
|
||||
if grep SPOT_API "$INCDIR/$file" >/dev/null; then
|
||||
:
|
||||
elif test -f "$SRCDIR/${file%.*}.cc"; then
|
||||
echo "FAIL: $file -- no exported symbol, should this file be private?"
|
||||
echo " $file" >> failures
|
||||
fi
|
||||
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
echo "Failed files:"
|
||||
cat failures
|
||||
rm failures
|
||||
exit 1;
|
||||
fi
|
||||
|
|
@ -1,98 +0,0 @@
|
|||
#! /usr/bin/perl -w
|
||||
# -*- cperl; coding: utf-8 -*-
|
||||
#
|
||||
# Copyright (C) 2010, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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/>.
|
||||
#
|
||||
# Check that all the directories documented in README exist, and that
|
||||
# all directories listed in configure.ac are documented.
|
||||
#
|
||||
# Also has an option --list to print directories which are
|
||||
# documented.
|
||||
|
||||
use strict;
|
||||
use warnings;
|
||||
|
||||
local $\ = "\n";
|
||||
my $top_srcdir = $ENV{top_srcdir} || "../../";
|
||||
my $top_srcdir_len = length($top_srcdir) + 1;
|
||||
my $list_mode = ($#ARGV != -1 && $ARGV[0] eq "--list");
|
||||
|
||||
unless (-f "$top_srcdir/README")
|
||||
{
|
||||
print STDERR "$top_srcdir/README not found";
|
||||
exit 2;
|
||||
}
|
||||
|
||||
open(FD, "$top_srcdir/README")
|
||||
or die "$!: cannot open $top_srcdir/README";
|
||||
my @directory = ();
|
||||
my $exit_status = 0;
|
||||
|
||||
my %documenteddirs;
|
||||
|
||||
while (<FD>)
|
||||
{
|
||||
# Skip non-distributed directories.
|
||||
next if /Not distributed/i;
|
||||
# We consider Third party software?
|
||||
# last if (/^Third party software$/);
|
||||
next unless (m{^(\s*)(\S+/)\s+});
|
||||
my $level = length($1) / 3;
|
||||
my $name = $2;
|
||||
|
||||
$directory[$level] = $name;
|
||||
$#directory = $level;
|
||||
my $filename = join "", @directory;
|
||||
|
||||
# Use globbing on the filename.
|
||||
for my $directory (glob("$top_srcdir/$filename"))
|
||||
{
|
||||
my $striped = substr($directory, $top_srcdir_len);
|
||||
$documenteddirs{$striped} = 1;
|
||||
if ($list_mode)
|
||||
{
|
||||
print "$striped";
|
||||
}
|
||||
else
|
||||
{
|
||||
unless (-d $directory || -f $directory)
|
||||
{
|
||||
print STDERR "$directory mentioned in README does not exist.";
|
||||
$exit_status = 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
close(FD);
|
||||
|
||||
open(FD, "$top_srcdir/configure.ac")
|
||||
or die "$!: cannot open $top_srcdir/configure.ac";
|
||||
while (<FD>)
|
||||
{
|
||||
next unless m{\s*(\S+/)Makefile};
|
||||
unless (exists $documenteddirs{$1})
|
||||
{
|
||||
print STDERR "$1 directory undocumented in README.";
|
||||
$exit_status = 1;
|
||||
}
|
||||
}
|
||||
close(FD);
|
||||
|
||||
exit $exit_status;
|
||||
|
|
@ -1,358 +0,0 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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
|
||||
|
||||
diag()
|
||||
{
|
||||
fail=:
|
||||
echo "$file:" "$@"
|
||||
echo ============================================================
|
||||
}
|
||||
|
||||
rm -f failures
|
||||
|
||||
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 him 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
|
||||
|
||||
tmp=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.
|
||||
for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do
|
||||
|
||||
find "$dir" \( -name "${1-*}.hh" \
|
||||
-o -name "${1-*}.hxx" \
|
||||
-o -name "${1-*}.cc" \
|
||||
-o -name "${1-*}.test" \) \
|
||||
-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
|
||||
|
||||
# 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 '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 '[ ]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 coma.'
|
||||
|
||||
# The 'r' allows operator&&
|
||||
# The '.' allows &&...
|
||||
$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 &&
|
||||
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.'
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
# 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.'
|
||||
;;
|
||||
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
|
||||
;;
|
||||
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
|
||||
|
||||
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
|
||||
done || : # Make sure sh does not abort when read exits with false.
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
echo "The following files contain style errors:"
|
||||
cat failures
|
||||
rm failures
|
||||
exit 1;
|
||||
fi
|
||||
|
||||
exit 0
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2015, 2016 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -24,7 +24,7 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
class mark_tools final
|
||||
class SPOT_API mark_tools final
|
||||
{
|
||||
public:
|
||||
/// \ingroup tl_rewriting
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
|
||||
## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
|
||||
## de Recherche et Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
|
||||
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -134,8 +134,6 @@ libtwaalgos_la_SOURCES = \
|
|||
tau03opt.cc \
|
||||
totgba.cc \
|
||||
translate.cc \
|
||||
weight.cc \
|
||||
weight.hh \
|
||||
word.cc
|
||||
|
||||
libtwaalgos_la_LIBADD = gtec/libgtec.la
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Copyright (C) 2011, 2013, 2014, 2015, 2016 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
|
||||
|
|
@ -49,7 +49,7 @@
|
|||
#include <spot/twaalgos/emptiness.hh>
|
||||
#include <spot/twaalgos/emptiness_stats.hh>
|
||||
#include <spot/twaalgos/tau03opt.hh>
|
||||
#include <spot/twaalgos/weight.hh>
|
||||
#include <spot/priv/weight.hh>
|
||||
#include <spot/twaalgos/ndfs_result.hxx>
|
||||
|
||||
namespace spot
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue