Run model checking during make check

configure.ac

@@ -198,6 +198,7 @@ if test x$enable_simgrid = xyes ; then
 			  CXXFLAGS="-std=c++11 $CXXFLAGS"
 			  NVCCFLAGS="-std=c++11 $NVCCFLAGS")
 	AC_LANG_POP([C++])
+	AC_PATH_PROG([SIMGRID_MC], [simgrid-mc])
 fi
 AM_CONDITIONAL(STARPU_SIMGRID, test x$enable_simgrid = xyes)
 AC_SUBST(SIMGRID_CFLAGS)
@@ -3075,6 +3076,7 @@ AC_SUBST(STARPU_EXPORTED_LIBS)
 AC_CONFIG_COMMANDS([executable-scripts], [
   chmod +x tests/regression/regression.sh
   chmod +x tests/loader-cross.sh
+  chmod +x tests/model-checking/prio_list.sh
   chmod +x examples/loader-cross.sh
   chmod +x examples/stencil/loader-cross.sh
   chmod +x gcc-plugin/tests/run-test
@@ -3179,6 +3181,7 @@ AC_OUTPUT([
 	examples/stencil/Makefile
 	tests/Makefile
 	tests/loader-cross.sh
+	tests/model-checking/prio_list.sh
 	examples/loader-cross.sh
 	examples/stencil/loader-cross.sh
 	mpi/Makefile

tests/Makefile.am

@@ -28,7 +28,7 @@ endif
 
 AM_CFLAGS = $(HWLOC_CFLAGS) $(FXT_CFLAGS) -Wall $(STARPU_CUDA_CPPFLAGS) $(STARPU_OPENCL_CPPFLAGS) $(STARPU_COI_CPPFLAGS) $(STARPU_SCIF_CPPFLAGS) $(GLOBAL_AM_CFLAGS) -Wno-unused
 AM_CXXFLAGS = $(HWLOC_CFLAGS) $(FXT_CFLAGS) -Wall $(STARPU_CUDA_CPPFLAGS) $(STARPU_OPENCL_CPPFLAGS) $(STARPU_COI_CPPFLAGS) $(STARPU_SCIF_CPPFLAGS) $(GLOBAL_AM_CXXFLAGS) -Wno-unused
-LIBS = $(top_builddir)/src/@LIBSTARPU_LINK@ $(HWLOC_LIBS) @LIBS@ $(FXT_LIBS)
+LDADD = $(top_builddir)/src/@LIBSTARPU_LINK@ $(HWLOC_LIBS) $(FXT_LIBS)
 AM_CPPFLAGS = -I$(top_srcdir)/include/ -I$(top_builddir)/src -I$(top_srcdir)/src/
 AM_LDFLAGS = @STARPU_EXPORT_DYNAMIC@ $(STARPU_OPENCL_LDFLAGS) $(STARPU_CUDA_LDFLAGS) $(STARPU_COI_LDFLAGS) $(STARPU_SCIF_LDFLAGS) $(FXT_LDFLAGS)
 
@@ -383,6 +383,16 @@ if STARPU_SIMGRID
 TESTS += $(MICROBENCHS:=.sh)
 endif
 
+if STARPU_SIMGRID
+model_checking_prio_list_LDADD = 
+model_checking_prio_list_LDFLAGS = 
+model_checking_prio_list_SOURCES = model-checking/prio_list.c ../src/common/rbtree.c
+noinst_PROGRAMS += model-checking/prio_list
+if !STARPU_QUICK_CHECK
+TESTS += model-checking/prio_list.sh
+endif
+endif
+
 TESTS += datawizard/locality.sh
 
 #######################

tests/model-checking/prio_list.sh.in

@@ -0,0 +1,36 @@
+#!/bin/bash -x
+#
+# StarPU --- Runtime system for heterogeneous multicore architectures.
+#
+# Copyright (C) 2017  Université de Bordeaux
+#
+# StarPU is free software; you can redistribute it and/or modify
+# it under the terms of the GNU Lesser General Public License as published by
+# the Free Software Foundation; either version 2.1 of the License, or (at
+# your option) any later version.
+#
+# StarPU 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 Lesser General Public License in COPYING.LGPL for more details.
+
+# Test prio_lists with simgrid model checker
+
+SIMGRID_MC=@SIMGRID_MC@
+abs_top_srcdir=@abs_top_srcdir@
+abs_builddir=@abs_builddir@
+
+set -e
+
+[ -x "$SIMGRID_MC" ] || exit 77
+
+MC_FLAGS=--cfg=model-check/reduction:none
+
+# makes it much longer actually
+#MC_FLAGS+=--cfg=contexts/factory:ucontext
+#MC_FLAGS+=--cfg=model-check/sparse-checkpoint:yes
+#MC_FLAGS+=--cfg=model-check/visited:1000
+
+PREFIX=$(dirname $0)
+$SIMGRID_MC $abs_builddir/prio_list $abs_top_srcdir/tests/model-checking/platform.xml MAIN $MC_FLAGS