model-checker : remove useless debug message and add another one

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 0e14bab..7042a58 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -237,7 +237,6 @@ static int compare_areas_with_type(void *area1, void *area2,
   case DW_TAG_structure_type:
   case DW_TAG_class_type:
     xbt_dynar_foreach(type->members, cursor, member) {
-      XBT_DEBUG("Compare member %s", member->name);
       void *member1 =
           mc_member_snapshot_resolve(area1, type, member, snapshot1);
       void *member2 =
@@ -375,9 +374,6 @@ static int compare_local_variables(mc_snapshot_t snapshot1,
       offset1 = (char *) current_var1->address - (char *) std_heap;
       offset2 = (char *) current_var2->address - (char *) std_heap;
       // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
-      XBT_DEBUG("Compare local variable %s of frame %s",
-                current_var1->subprogram->name, current_var1->subprogram->name);
-
 
       if (current_var1->region == 1) {
         dw_type_t subtype = current_var1->type;

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index d68a78b..a77883f 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -212,6 +212,8 @@ void MC_modelcheck_safety(void)
           XBT_DEBUG("User max depth reached !");
         else if (visited_state == -1)
           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+        else
+          XBT_DEBUG("State already visited, exploration stopped on this path.");
 
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           /* Interleave enabled processes in the state in which they have been enabled for the first time */