diff --git a/README b/README index d654d35b0..b8080794c 100644 --- a/README +++ b/README @@ -148,13 +148,13 @@ spot/ Sources for libspot. twa/ TωA objects and cousins (Transition-based ω-Automata). twaalgos/ Algorithms on TωA. gtec/ Couvreur's Emptiness-Check. - sanity/ Sanity tests for the whole project. bin/ Command-line tools built on top of libspot. man/ Man pages for the above tools. tests/ Test suite. core/ Tests for libspot and the binaries. ltsmin/ Tests for the DiVinE2/SpinS interface. python/ Tests for Python bindings. + sanity/ Tests for the coherence of the source base. doc/ Documentation for Spot. org/ Source of userdoc/ as org-mode files. tl/ Documentation of the Temporal Logic operators. diff --git a/configure.ac b/configure.ac index c713cf24b..8285cf50a 100644 --- a/configure.ac +++ b/configure.ac @@ -1,6 +1,6 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -# de Recherche et Développement de l'Epita (LRDE). +# 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, 2006, 2007 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis # Coopératifs (SRC), Université Pierre et Marie Curie. @@ -209,7 +209,6 @@ AC_CONFIG_FILES([ spot/parseaut/Makefile spot/parsetl/Makefile spot/priv/Makefile - spot/sanity/Makefile spot/taalgos/Makefile spot/ta/Makefile spot/tl/Makefile diff --git a/spot/Makefile.am b/spot/Makefile.am index 54e27696c..6d48c44e0 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -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 = diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am index a42dd0880..82ec970cf 100644 --- a/spot/priv/Makefile.am +++ b/spot/priv/Makefile.am @@ -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 diff --git a/spot/twaalgos/weight.cc b/spot/priv/weight.cc similarity index 93% rename from spot/twaalgos/weight.cc rename to spot/priv/weight.cc index dfafd9d91..80938889d 100644 --- a/spot/twaalgos/weight.cc +++ b/spot/priv/weight.cc @@ -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 #include -#include +#include namespace spot { diff --git a/spot/twaalgos/weight.hh b/spot/priv/weight.hh similarity index 100% rename from spot/twaalgos/weight.hh rename to spot/priv/weight.hh diff --git a/spot/sanity/Makefile.am b/spot/sanity/Makefile.am deleted file mode 100644 index 71463dbf6..000000000 --- a/spot/sanity/Makefile.am +++ /dev/null @@ -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 . - -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 diff --git a/spot/tl/mark.hh b/spot/tl/mark.hh index 26e8bc2ef..ee917a440 100644 --- a/spot/tl/mark.hh +++ b/spot/tl/mark.hh @@ -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 diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index a44976d21..02734f892 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -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 diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index 2c2a77e6e..f485dc3d5 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -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 #include #include -#include +#include #include namespace spot diff --git a/tests/Makefile.am b/tests/Makefile.am index e26a8b00b..9257ed4ef 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -26,7 +26,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/spot/libspot.la -TEST_EXTENTIONS = .test .py .ipynb +TEST_EXTENTIONS = .test .py .ipynb .pl LOG_COMPILER = ./run TEST_LOG_COMPILER = ./run @@ -36,8 +36,8 @@ check_SCRIPTS = run # We try to keep this somehow by strength. Test basic things first, # because such failures will be easier to diagnose and fix. -TESTS = $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) \ - $(TESTS_python) $(TESTS_ltsmin) +TESTS = $(TESTS_sanity) $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) \ + $(TESTS_twa) $(TESTS_python) $(TESTS_ltsmin) distclean-local: rm -rf $(TESTS:.test=.dir) @@ -334,3 +334,14 @@ TESTS_ltsmin = \ EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/finite.dve ltsmin/finite.pm ltlsmin/kripke.log: core/parse_print$(EXEEXT) + + +############################## SANITY ############################## + +TESTS_sanity = \ + sanity/80columns.test \ + sanity/includes.test \ + sanity/ipynb.pl \ + sanity/private.test \ + sanity/readme.pl \ + sanity/style.test diff --git a/tests/run.in b/tests/run.in index 23465263b..6973279ff 100755 --- a/tests/run.in +++ b/tests/run.in @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2014, 2015, 2016 Laboratoire de Recherche et # Developpement 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é @@ -77,6 +77,8 @@ case $1 in exec $PREFIXCMD @PYTHON@ "$@";; *.test) exec sh -x "$@";; + *.pl) + exec @PERL@ "$@";; *python*) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ exec $PREFIXCMD "$@";; diff --git a/spot/sanity/.gitignore b/tests/sanity/.gitignore similarity index 100% rename from spot/sanity/.gitignore rename to tests/sanity/.gitignore diff --git a/spot/sanity/80columns.test b/tests/sanity/80columns.test similarity index 95% rename from spot/sanity/80columns.test rename to tests/sanity/80columns.test index 491e92c17..cfab94180 100755 --- a/spot/sanity/80columns.test +++ b/tests/sanity/80columns.test @@ -42,11 +42,12 @@ 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 +for dir in "${srcdir-.}/../../spot" "${srcdir-.}/.."; do find "$dir" \( -name "${1-*}.hh" \ -o -name "${1-*}.hxx" \ -o -name "${1-*}.cc" \ + -o -name "${1-*}.py" \ -o -name "${1-*}.test" \) -a -type f -a -print | while read file; do if (expand $file | grep -q $x) 2>/dev/null; then diff --git a/spot/sanity/includes.test b/tests/sanity/includes.test similarity index 94% rename from spot/sanity/includes.test rename to tests/sanity/includes.test index ec6ddfdf4..efd74505f 100755 --- a/spot/sanity/includes.test +++ b/tests/sanity/includes.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2008, 2011, 2012 Laboratoire de Recherche et +# Copyright (C) 2008, 2011, 2012, 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é @@ -27,8 +27,8 @@ set -e rm -f failures -# Remove any trailing slash -INCDIR=${INCDIR%/} + +INCDIR=${srcdir-.}/../../spot for file in `find "$INCDIR" \( -name "${1-*}.hh" \ -o -name "${1-*}.hxx" \) \ diff --git a/spot/sanity/ipynb.test b/tests/sanity/ipynb.pl similarity index 84% rename from spot/sanity/ipynb.test rename to tests/sanity/ipynb.pl index f5afb6f15..ab9f74f90 100755 --- a/spot/sanity/ipynb.test +++ b/tests/sanity/ipynb.pl @@ -1,7 +1,7 @@ #! /usr/bin/perl -w # -*- cperl; coding: utf-8 -*- # -# Copyright (C) 2010, 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -29,11 +29,10 @@ use strict; use warnings; local $\ = "\n"; -my $top_srcdir = $ENV{top_srcdir} || "../../"; -my $top_srcdir_len = length($top_srcdir) + 1; +my $srcdir = $ENV{srcdir} || "."; -my $tut = "$top_srcdir/doc/org/tut.org"; -my $dir = "$top_srcdir/tests/python"; +my $tut = "$srcdir/../../doc/org/tut.org"; +my $dir = "$srcdir/../../tests/python"; unless (-f $tut) { print STDERR "$tut not found"; @@ -51,7 +50,7 @@ while () $seen{$1} = 1; unless (-f "$dir/$1") { - print STDERR "notebook mentioned in tut.org does not exist"; + print STDERR "notebook $1 mentioned in tut.org does not exist"; $exit_status = 1; } } @@ -73,4 +72,6 @@ while () } close(FD); +die "No notebook found?" if scalar(keys %seen) == 0; + exit $exit_status; diff --git a/spot/sanity/private.test b/tests/sanity/private.test similarity index 73% rename from spot/sanity/private.test rename to tests/sanity/private.test index 67eab6b06..ba0d658f9 100755 --- a/spot/sanity/private.test +++ b/tests/sanity/private.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013 Laboratoire de Recherche et +# Copyright (C) 2013, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -27,25 +27,29 @@ set -e rm -f failures -# Remove any trailing slash -INCDIR=${INCDIR%/} + +INCDIR=${srcdir-.}/../../spot for file in `find "$INCDIR" \( -name "${1-*}.hh" \ - -o -name "${1-*}.hxx" \) \ + -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 - + case $file in + priv/*) ;; + *) + if grep -E -q '(SPOT_API|GNU Bison)' "$INCDIR/$file"; then + : + elif test -f "$INCDIR/${file%.*}.cc"; then + echo "FAIL: $file -- no exported symbol, should this file be private?" + echo " $file" >> failures + fi + ;; + esac done if test -f failures; then echo "Failed files:" cat failures rm failures - exit 1; + exit 1 fi diff --git a/spot/sanity/readme.test b/tests/sanity/readme.pl similarity index 93% rename from spot/sanity/readme.test rename to tests/sanity/readme.pl index 226c2db44..bfbc85c64 100755 --- a/spot/sanity/readme.test +++ b/tests/sanity/readme.pl @@ -1,8 +1,8 @@ #! /usr/bin/perl -w # -*- cperl; coding: utf-8 -*- # -# Copyright (C) 2010, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2010, 2015, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -29,7 +29,8 @@ use strict; use warnings; local $\ = "\n"; -my $top_srcdir = $ENV{top_srcdir} || "../../"; +my $srcdir = $ENV{srcdir} || "."; +my $top_srcdir = "$srcdir/../.."; my $top_srcdir_len = length($top_srcdir) + 1; my $list_mode = ($#ARGV != -1 && $ARGV[0] eq "--list"); diff --git a/spot/sanity/style.test b/tests/sanity/style.test similarity index 96% rename from spot/sanity/style.test rename to tests/sanity/style.test index f6fc0e795..5bd975f37 100755 --- a/spot/sanity/style.test +++ b/tests/sanity/style.test @@ -1,7 +1,7 @@ #! /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) 2009, 2010, 2011, 2012, 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 et Marie Curie. @@ -44,18 +44,20 @@ if (grep --color=auto -n --version)>/dev/null 2>&1; then 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, +# 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 -tmp=incltest.tmp +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. -for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do +TOP=${srcdir-.}/../.. +for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do find "$dir" \( -name "${1-*}.hh" \ -o -name "${1-*}.hxx" \