XBT_INFO(" %s", s.c_str());
simgrid::mc::dumpRecordPath();
simgrid::mc::session->log_state();
- XBT_INFO("Stack trace:");
- mc_model_checker->process().dump_stack();
+ if (xbt_log_no_loc) {
+ XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
+ } else {
+ XBT_INFO("Stack trace:");
+ mc_model_checker->process().dump_stack();
+ }
}
static void MC_report_assertion_error()
+# MC-only C++ binaries
foreach(x dwarf dwarf-expression)
if (SIMGRID_HAVE_MC)
add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.cpp)
set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.cpp)
endforeach()
+# MC-independent C++ binaries
+foreach(x random-bug)
+ add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.cpp)
+ target_link_libraries(${x} simgrid)
+ set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x})
+ set_property(TARGET ${x} APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}")
+ add_dependencies(tests ${x})
+
+ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.tesh)
+ set(teshsuite_src ${teshsuite_src} ${CMAKE_CURRENT_SOURCE_DIR}/${x}/${x}.cpp)
+endforeach()
+
add_executable (without-mutex-handling EXCLUDE_FROM_ALL mutex-handling/mutex-handling.c)
target_link_libraries(without-mutex-handling simgrid)
set_target_properties(without-mutex-handling PROPERTIES COMPILE_FLAGS -DDISABLE_THE_MUTEX=1)
set_target_properties(without-mutex-handling PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/mutex-handling)
add_dependencies(tests without-mutex-handling)
-foreach(x mutex-handling random-bug)
+foreach(x mutex-handling)
add_executable (${x} EXCLUDE_FROM_ALL ${x}/${x}.c)
target_link_libraries(${x} simgrid)
set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x})
endforeach()
set(teshsuite_src ${teshsuite_src} PARENT_SCOPE)
-set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/random-bug/random-bug-report.tesh
+set(tesh_files ${tesh_files} ${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)
# 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-record --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug-report.tesh)
+ 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)
ENDIF()
-ADD_TESH(mc-random-bug --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/random-bug --setenv srcdir=${CMAKE_HOME_DIRECTORY} --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/random-bug random-bug.tesh)
+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)
--- /dev/null
+#!/usr/bin/env tesh
+$ ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4"
+> Behavior: printf
+> [ 0.000000] (0:maestro@) path=1/3;1/4
+> Error reached
+
+# Behavior: assert does not have the same output within and without MC, so don't test it here. That's already covered with the other ones
+
+! expect signal SIGIOT
+$ ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4"
+> Behavior: abort
+> [ 0.000000] (0:maestro@) path=1/3;1/4
+++ /dev/null
-#!/usr/bin/env tesh
-! expect return 1
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/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@) **************************
-> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
-> [ 0.000000] (0:maestro@) **************************
-> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) [(1)Tremblay (app)] MC_RANDOM(3)
-> [ 0.000000] (0:maestro@) [(1)Tremblay (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
+++ /dev/null
-/* Copyright (c) 2014-2019. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <simgrid/msg.h>
-#include <simgrid/modelchecker.h>
-
-#include <stdio.h> /* snprintf */
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application");
-
-/** An (fake) application with a bug occuring for some random values */
-static int app(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[])
-{
- int x = MC_random(0, 5);
- int y = MC_random(0, 5);
-
- if (MC_is_active()) {
- MC_assert(x !=3 || y !=4);
- }
- if (x ==3 && y ==4) {
- fprintf(stderr, "Error reached\n");
- }
-
- return 0;
-}
-
-/** Main function */
-int main(int argc, char *argv[])
-{
- MSG_init(&argc, argv);
- MSG_function_register("app", &app);
- MSG_create_environment(argv[1]);
- MSG_process_create("app", app, NULL, MSG_get_host_by_name("Tremblay"));
- return MSG_main();
-}
--- /dev/null
+/* Copyright (c) 2014-2019. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+#include <stdio.h> /* snprintf */
+
+enum { ABORT, ASSERT, PRINTF } behavior;
+
+/** An (fake) application with a bug occuring for some random values */
+static void app()
+{
+ int x = MC_random(0, 5);
+ int y = MC_random(0, 5);
+
+ if (behavior == ABORT) {
+ abort();
+ } else if (behavior == ASSERT) {
+ MC_assert(x != 3 || y != 4);
+ } else if (behavior == PRINTF) {
+ if (x == 3 && y == 4)
+ fprintf(stderr, "Error reached\n");
+ }
+}
+
+/** Main function */
+int main(int argc, char* argv[])
+{
+ simgrid::s4u::Engine e(&argc, argv);
+ xbt_assert(argc == 3, "Usage: random-bug raise|assert <platformfile>");
+ if (strcmp(argv[1], "abort") == 0) {
+ printf("Behavior: abort\n");
+ behavior = ABORT;
+ } else if (strcmp(argv[1], "assert") == 0) {
+ printf("Behavior: assert\n");
+ behavior = ASSERT;
+ } else if (strcmp(argv[1], "printf") == 0) {
+ printf("Behavior: printf\n");
+ behavior = PRINTF;
+ }
+
+ e.load_platform(argv[2]);
+
+ simgrid::s4u::Actor::create("app", simgrid::s4u::Host::by_name("Fafard"), &app);
+ e.run();
+}
#!/usr/bin/env tesh
-$ ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4"
-> [ 0.000000] (0:maestro@) path=1/3;1/4
+! 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.
+> 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
+
+! expect return 6
+# because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
+> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
+> Behavior: abort
+> [ 0.000000] (0:maestro@) **************************
+> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
+> [ 0.000000] (0:maestro@) **************************
+> [ 0.000000] (0:maestro@) From signal: Aborted
+> [ 0.000000] (0:maestro@) No core dump was generated by the system.
+> [ 0.000000] (0:maestro@) Counter-example execution trace:
+> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(0)
+> [ 0.000000] (0:maestro@) [(1)Fafard (app)] MC_RANDOM(0)
+> [ 0.000000] (0:maestro@) Path = 1;1
+> [ 0.000000] (0:maestro@) Expanded states = 2
+> [ 0.000000] (0:maestro@) Visited states = 2
+> [ 0.000000] (0:maestro@) Executed transitions = 2
+> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
+
+$ ${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.
+> Behavior: printf
> 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