Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Dry run MC examples for coverage.
authorArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Thu, 3 Dec 2020 22:15:57 +0000 (23:15 +0100)
committerArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Thu, 3 Dec 2020 22:16:10 +0000 (23:16 +0100)
examples/s4u/CMakeLists.txt
teshsuite/mc/CMakeLists.txt

index c449b48..f8ec744 100644 (file)
@@ -47,7 +47,6 @@ if(SIMGRID_HAVE_MC)
     set_target_properties(s4u-mc-bugged1-liveness-cleaner-off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner")
     add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-off)
   endif()
     set_target_properties(s4u-mc-bugged1-liveness-cleaner-off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner")
     add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-off)
   endif()
-
 endif()
 
 if(SIMGRID_HAVE_NS3)
 endif()
 
 if(SIMGRID_HAVE_NS3)
@@ -207,6 +206,17 @@ if (NOT enable_memcheck AND NOT WIN32)
                             ${CMAKE_CURRENT_SOURCE_DIR}/app-pingpong/simix-breakpoint.tesh)
 endif()
 
                             ${CMAKE_CURRENT_SOURCE_DIR}/app-pingpong/simix-breakpoint.tesh)
 endif()
 
+if(enable_coverage)
+  foreach (example mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert)
+    if(NOT DEFINED _${example}_disable)
+      ADD_TEST(cover-${example} ${CMAKE_CURRENT_BINARY_DIR}/${example}/s4u-${example} ${CMAKE_HOME_DIRECTORY}/examples/platforms/model_checker_platform.xml)
+    endif()
+  endforeach()
+  if(SIMGRID_HAVE_MC)
+    add_test(cover-mc-bugged1-liveness ${CMAKE_CURRENT_BINARY_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml 0 1000)
+  endif()
+endif()
+
 # Add all extra files to the archive
 ####################################
 
 # Add all extra files to the archive
 ####################################
 
index 451a0ea..d5e9044 100644 (file)
@@ -50,3 +50,7 @@ IF(SIMGRID_HAVE_MC)
 ENDIF()
 
 ADD_TESH(mc-random-bug-replay                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh)
 ENDIF()
 
 ADD_TESH(mc-random-bug-replay                  --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-replay.tesh)
+
+if(enable_coverage)
+  add_test(cover-mc-mutex-handling ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling/mutex-handling ${CMAKE_HOME_DIRECTORY}/examples/platforms/small_platform.xml)
+endif()