model-checker : fix segfault in get_local_variables_values()

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

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 3d89d84..cdd8c33 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -11,11 +11,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
 static char* pointer_to_string(void* pointer);
 static char* buff_size_to_string(size_t size);
 
-int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
-{
-  if(_surf_do_model_check == 2)
+int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
+  if(mc_reduce_kind == e_mc_reduce_none)
     return TRUE;
-  
+
 
   if (r1->issuer == r2->issuer)
     return FALSE;
@@ -240,6 +239,16 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MC_SNAPSHOT:
+    type = xbt_strdup("MC_SNAPSHOT");
+    args = '\0';
+    break;
+
+  case SIMCALL_MC_COMPARE_SNAPSHOTS:
+    type = xbt_strdup("MC_COMPARE_SNAPSHOTS");
+    args = '\0';
+    break;
+
   default:
     THROW_UNIMPLEMENTED;
   }
@@ -272,7 +281,9 @@ int MC_request_is_visible(smx_simcall_t req)
     || req->call == SIMCALL_COMM_WAIT
     || req->call == SIMCALL_COMM_WAITANY
     || req->call == SIMCALL_COMM_TEST
-    || req->call == SIMCALL_COMM_TESTANY;
+    || req->call == SIMCALL_COMM_TESTANY
+    || req->call == SIMCALL_MC_SNAPSHOT
+    || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS;
 }
 
 int MC_request_is_enabled(smx_simcall_t req)
@@ -289,7 +300,12 @@ int MC_request_is_enabled(smx_simcall_t req)
      * communication is not ready, it can timeout and won't block.
      * On the other hand if it hasn't a timeout, check if the comm is ready.*/
     if(req->comm_wait.timeout >= 0){
-      return TRUE;
+      if(_surf_mc_timeout == 1){
+        return TRUE;
+      }else{
+        act = req->comm_wait.comm;
+        return (act->comm.src_proc && act->comm.dst_proc);
+      }
     }else{
       act = req->comm_wait.comm;
       return (act->comm.src_proc && act->comm.dst_proc);