Add a sanity check for installed private headers.

If an installed header has an associated *.cc file (in the source
tree), but does not declare any SPOT_API symbol, something is fishy.
Either that header should not be installed, or it is missing the
SPOT_API markers.

* src/sanity/private.test: New test.
* src/sanity/Makefile.am: Call it.
* src/ltlast/Makefile.am: Do not install formula_tree.hh.
* src/ltlvisit/Makefile.am: Do not install mark.hh.
* src/tgbaalgos/Makefile.am: Do not intall weight.hh.

src/ltlast/Makefile.am

@@ -33,7 +33,6 @@ ltlast_HEADERS = \
   bunop.hh \
   constant.hh \
   formula.hh \
-  formula_tree.hh \
   multop.hh \
   nfa.hh \
   predecl.hh \
@@ -50,6 +49,7 @@ libltlast_la_SOURCES = \
   constant.cc \
   formula.cc \
   formula_tree.cc \
+  formula_tree.hh \
   multop.cc \
   nfa.cc \
   refformula.cc \

src/ltlvisit/Makefile.am

@@ -35,7 +35,6 @@ ltlvisit_HEADERS = \
   lbt.hh \
   length.hh \
   lunabbrev.hh \
-  mark.hh \
   nenoform.hh \
   postfix.hh \
   randomltl.hh \
@@ -61,6 +60,7 @@ libltlvisit_la_SOURCES = \
   length.cc \
   lunabbrev.cc \
   mark.cc \
+  mark.hh \
   nenoform.cc \
   postfix.cc \
   randomltl.cc \

src/sanity/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+## Copyright (C) 2010, 2011, 2012, 2013 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
@@ -51,13 +51,21 @@ check-local: check-80columns check-style check-readme check-includes
 
 
 # Ensure we have not forgotten to include an header.
-installcheck-local:
+check-installed-includes:
 	CXX='$(CXX)' \
 	CPPFLAGS='-I $(includedir) -I$(pkgincludedir) $(LIBGSPN_CPPFLAGS) $(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 = includes.test 80columns.test style.test readme.test
+EXTRA_DIST = includes.test 80columns.test style.test readme.test private.test

src/sanity/private.test

@@ -0,0 +1,33 @@
+#! /bin/sh
+
+# 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

src/tgbaalgos/Makefile.am

@@ -68,8 +68,7 @@ tgbaalgos_HEADERS = \
   tau03.hh \
   tau03opt.hh \
   translate.hh \
-  reductgba_sim.hh \
+  reductgba_sim.hh
-  weight.hh
 
 noinst_LTLIBRARIES = libtgbaalgos.la
 libtgbaalgos_la_SOURCES = \
@@ -114,6 +113,7 @@ libtgbaalgos_la_SOURCES = \
   tau03opt.cc \
   translate.cc \
   reductgba_sim.cc \
-  weight.cc
+  weight.cc \
+  weight.hh
 
 libtgbaalgos_la_LIBADD = gtec/libgtec.la