From 29b2bf945239b1950c277f4afff78e8ea327000a Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 4 Jun 2014 17:13:23 +0200 Subject: [PATCH 1/1] model-checker : remove useless debug message and add another one --- src/mc/mc_compare.c | 4 ---- src/mc/mc_safety.c | 2 ++ 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 0e14bab653..7042a5854b 100644 --- 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 d68a78b30a..a77883fdcc 100644 --- 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 */ -- 2.20.1