X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/32dd95e241a3e08572df4f19f6603551ed5dbd63..41a79ecaf5ce51f0513500e8cc7f9a0ed5435374:/teshsuite/smpi/isp/umpire/CMakeLists.txt?ds=sidebyside

diff --git a/teshsuite/smpi/isp/umpire/CMakeLists.txt b/teshsuite/smpi/isp/umpire/CMakeLists.txt
index 6cb426be04..1200f99eef 100644
--- a/teshsuite/smpi/isp/umpire/CMakeLists.txt
+++ b/teshsuite/smpi/isp/umpire/CMakeLists.txt
@@ -1,10 +1,6 @@
 # See http://formalverification.cs.utah.edu/ISP_Tests/
 
 set(umpire_tests_passing
-  any_src-can-deadlock
-  any_src-can-deadlock2
-  any_src-can-deadlock3
-  any_src-deadlock
   change-send-buffer
   comm-dup-no-error
   comm-dup-no-free
@@ -35,12 +31,21 @@ set(umpire_tests_passing
   partial-recv
   sendrecv-deadlock
   send-recv-ok
-  waitall-deadlock
-  waitany-deadlock
-  wait-deadlock
+  irecv-isend-ok
+  irecv-isend-ok2
+  lost-request-waitall
  ) # Passing (no deadlock) tests
- 
-set(umpire_tests_failing
+
+# These are supposed to deadlock but ISP does not find deadlock
+# and we don't either. What should be test here?
+set(umpire_tests_missed_deadlock
+  any_src-deadlock
+  any_src-can-deadlock
+  any_src-can-deadlock2
+  any_src-can-deadlock3
+  )
+
+set(umpire_tests_deadlock
   any_src-can-deadlock10
   any_src-can-deadlock10_mod
   any_src-can-deadlock11
@@ -74,10 +79,9 @@ set(umpire_tests_failing
   dropped-req
   finalize-deadlock
   irecv-deadlock
-  irecv-isend-ok
-  irecv-isend-ok2
-  lost-request-waitall
-
+  waitall-deadlock
+  waitany-deadlock
+  wait-deadlock
  ) # failing (deadlocking) tests
  
 set(umpire_tests_problematic
@@ -136,7 +140,7 @@ set(umpire_src_other
   no-error-probe-any_tag.c
   no-error-probe.c
   
-  # no-error-wait2.c # Does not compile.
+  no-error-wait2.c # Does not compile.
   no-error-waitall-any_src2.c
   no-error-waitall-any_src3.c
   no-error-waitall-any_src.c
@@ -169,29 +173,23 @@ set(umpire_src_other
   type-no-free-exhaustive.c
   )
 
-# Add every file to the archive
-###############################
-
-set(sources "")
-foreach(s ${umpire_src_other})
-  set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${s})
-endforeach()
+# Add these files to the archive
+#################
 
-foreach(file ${umpire_tests_passing} ${umpire_tests_failing} ${umpire_tests_problematic}  ) 
+set(sources "${CMAKE_CURRENT_SOURCE_DIR}/README")
+foreach(file ${umpire_src_other})
   set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file})
 endforeach()
 
+foreach(file ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_missed_deadlock} ${umpire_tests_problematic}  ) 
+  set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file}.c)
+endforeach()
+set(txt_files ${txt_files} ${sources} PARENT_SCOPE)
 
 # Build the tests
 #################
 
-set(umpire_tesh "")
-# set(examples_src ${examples_src} ${sources} PARENT_SCOPE)
-set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/README PARENT_SCOPE)
-# set(EXTRA_DIST ${EXTRA_DIST} ${CMAKE_CURRENT_SOURCE_DIR}/no-error-wait2.c PARENT_SCOPE)
-# set(tesh_files ${tesh_files} ${umpire_tesh} PARENT_SCOPE)
-
-if(enable_smpi AND enable_smpi_ISP_testsuite)
+if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
   set(CMAKE_C_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpicc")
   set(CMAKE_Fortran_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpiff")
 
@@ -199,7 +197,7 @@ if(enable_smpi AND enable_smpi_ISP_testsuite)
 
   include_directories(BEFORE "${CMAKE_HOME_DIRECTORY}/include/smpi")
 
-  foreach (test ${umpire_tests_passing} ${umpire_tests_failing} ${umpire_tests_problematic} )
+  foreach (test ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_problematic} )
     add_executable(${test} ${test}.c)
     target_link_libraries(${test} simgrid)
     set_source_files_properties(${test}.c PROPERTIES COMPILE_FLAGS "-Wno-error")
@@ -207,13 +205,15 @@ if(enable_smpi AND enable_smpi_ISP_testsuite)
     set(files_to_clean ${files_to_clean} ${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh)
   endforeach(test)
   
-  foreach (test ${umpire_tests_passing} )
+  # TODO, what should we do about ${umpire_tests_missed_deadlock}?
+
+  foreach (test ${umpire_tests_passing})
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30")
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display" APPEND)
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
   endforeach()
 
-  foreach (test ${umpire_tests_failing} ${umpire_tests_problematic} )
+  foreach (test ${umpire_tests_deadlock} ${umpire_tests_problematic} )
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30"     )
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! expect return 3" APPEND)
     write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display"  APPEND)
@@ -224,7 +224,7 @@ endif()
 # Erase all tesh files on cleanup: they are generated anyway
 set_directory_properties ( PROPERTIES ADDITIONAL_MAKE_CLEAN_FILES "${files_to_clean}" )
 
-if(enable_smpi AND enable_smpi_ISP_testsuite)
+if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
   foreach (tesh ${umpire_tesh})
     ADD_TESH(mc-umpire-${tesh}
       --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}