[mc] Do not take NULL to mean 'the current address space' in dwarf expressions

[simgrid.git] / src / mc / mc_safety.c

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 2aafad6..3dea427 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -11,12 +11,27 @@
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
+#include "mc_smx.h"
 
 #include "xbt/mmalloc/mmprivate.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
+static int is_exploration_stack_state(mc_state_t current_state){
+
+  xbt_fifo_item_t item;
+  mc_state_t stack_state;
+  for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+    stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    if(snapshot_compare(stack_state, current_state) == 0){
+      XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+      return 1;
+    }
+  }
+  return 0;
+}
+
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
@@ -112,6 +127,11 @@ void MC_modelcheck_safety(void)
 
       next_state = MC_state_new();
 
+      if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+          MC_show_non_termination();
+          return;
+      }
+
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
@@ -188,7 +208,7 @@ void MC_modelcheck_safety(void)
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
-          const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
@@ -217,7 +237,7 @@ void MC_modelcheck_safety(void)
 
             } else {
 
-              const smx_process_t previous_issuer = MC_process_get_issuer(&mc_model_checker->process, MC_state_get_internal_request(prev_state));
+              const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
                         req->call, issuer->pid, state->num,
                         MC_state_get_internal_request(prev_state)->call,