From: Frederic Suter Date: Wed, 10 Jul 2019 10:20:47 +0000 (+0200) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.24~348 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0ae0dc6c811f90a65c57d3b551424d326e2da264?hp=a31a5aabed1a30637c9ccdd30361b1eda8155968 Merge branch 'master' of https://framagit.org/simgrid/simgrid --- diff --git a/MANIFEST.in b/MANIFEST.in index b58b8948a4..75b07232f5 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -557,6 +557,7 @@ include teshsuite/mc/mutex-handling/mutex-handling.c include teshsuite/mc/mutex-handling/mutex-handling.tesh include teshsuite/mc/mutex-handling/mutex-handling_d.xml include teshsuite/mc/mutex-handling/without-mutex-handling.tesh +include teshsuite/mc/random-bug/random-bug-nocrash.tesh include teshsuite/mc/random-bug/random-bug-replay.tesh include teshsuite/mc/random-bug/random-bug.cpp include teshsuite/mc/random-bug/random-bug.tesh diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 338c107806..0bd8683d1e 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -338,7 +338,10 @@ void ModelChecker::handle_waitpid() xbt_die("Could not PTRACE_CONT"); } - else if (WIFEXITED(status) || WIFSIGNALED(status)) { + else if (WIFSIGNALED(status)) { + MC_report_crash(status); + mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); + } else if (WIFEXITED(status)) { XBT_DEBUG("Child process is over"); this->process().terminate(); } diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 86820cdcaa..f7fdd36cea 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -41,7 +41,8 @@ foreach(x mutex-handling) endforeach() set(teshsuite_src ${teshsuite_src} PARENT_SCOPE) -set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh +set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-nocrash.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-replay.tesh ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/without-mutex-handling.tesh PARENT_SCOPE) set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/mutex-handling/mutex-handling_d.xml PARENT_SCOPE) @@ -52,7 +53,11 @@ IF(SIMGRID_HAVE_MC) # ADD_TESH(tesh-mc-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling mutex-handling.tesh --cfg=model-check/reduction:dpor) ADD_TESH(tesh-mc-without-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:none) ADD_TESH(tesh-mc-without-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/mutex-handling --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/mutex-handling without-mutex-handling.tesh --cfg=model-check/reduction:dpor) - ADD_TESH(mc-random-bug --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.tesh) + IF("${CMAKE_SYSTEM}" MATCHES "Linux") + ADD_TESH(mc-random-bug --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.tesh) + ELSE() + ADD_TESH(mc-random-bug-nocrash --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-nocrash.tesh) + ENDIF() 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) diff --git a/teshsuite/mc/random-bug/random-bug-nocrash.tesh b/teshsuite/mc/random-bug/random-bug-nocrash.tesh new file mode 100644 index 0000000000..00fdd65fe1 --- /dev/null +++ b/teshsuite/mc/random-bug/random-bug-nocrash.tesh @@ -0,0 +1,24 @@ +#!/usr/bin/env tesh +! expect return 1 +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> [ 0.000000] (0:maestro@) Behavior: assert +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID *** +> [ 0.000000] (0:maestro@) ************************** +> [ 0.000000] (0:maestro@) Counter-example execution trace: +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(3) +> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(4) +> [ 0.000000] (0:maestro@) Path = 1/3;1/4 +> [ 0.000000] (0:maestro@) Expanded states = 27 +> [ 0.000000] (0:maestro@) Visited states = 68 +> [ 0.000000] (0:maestro@) Executed transitions = 46 + +$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning +> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor. +> [ 0.000000] (0:maestro@) Behavior: printf +> [ 0.000000] (1:app@Fafard) Error reached +> [ 0.000000] (0:maestro@) No property violation found. +> [ 0.000000] (0:maestro@) Expanded states = 43 +> [ 0.000000] (0:maestro@) Visited states = 108 +> [ 0.000000] (0:maestro@) Executed transitions = 72