From 606fd6074429a2b25a185ba92dce29759ab41255 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 3 Jun 2014 19:00:53 +0200 Subject: [PATCH 1/1] model-checker : comment erroneous ignore (not completely sure ...) --- examples/msg/mc/bugged1_liveness.tesh | 14 ++++++-------- src/mc/mc_global.c | 4 ++-- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index ff3cd799cc..fce5786e53 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -15,7 +15,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle > [ 0.000000] (3:client@Fafard) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly -> [ 0.000000] (0:@) Pair 21 already reached (equal to pair 9) ! +> [ 0.000000] (0:@) Pair 22 already reached (equal to pair 10) ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* > [ 0.000000] (0:@) | ACCEPTANCE CYCLE | > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* @@ -40,10 +40,8 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../msg_platform.xml ${srcdir:=.}/de > [ 0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) > [ 0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only)) > [ 0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)]) -> [ 0.000000] (0:@) Expanded pairs = 21 -> [ 0.000000] (0:@) Visited pairs = 21 -> [ 0.000000] (0:@) Executed transitions = 20 -> [ 0.000000] (0:@) Counter-example depth : 20 - - - +> [ 0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only)) +> [ 0.000000] (0:@) Expanded pairs = 22 +> [ 0.000000] (0:@) Visited pairs = 22 +> [ 0.000000] (0:@) Executed transitions = 21 +> [ 0.000000] (0:@) Counter-example depth : 21 diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 887aedcd02..f9286fe511 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -280,11 +280,11 @@ void MC_init() MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - smx_process_t process; + /*smx_process_t process; xbt_swag_foreach(process, simix_global->process_list) { MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup)); - } + }*/ } if (raw_mem_set) -- 2.20.1