From: Brian Norris Date: Mon, 28 May 2012 19:12:04 +0000 (-0700) Subject: clockvector: fixup initialization X-Git-Tag: pldi2013~392^2~13 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=73cd0247207fb071effa55b9f39e3db711412d96;p=model-checker.git clockvector: fixup initialization Two related fixes: Even if parent is NULL, pass the current ModelAction to ClockVector constructor. When no parent is present, do not make special case for initializing clock[0] = 1. This is only correct for a single case (the root Action) and is already handled in other ways. --- diff --git a/action.cc b/action.cc index 73d4c49..d76796d 100644 --- a/action.cc +++ b/action.cc @@ -88,7 +88,7 @@ void ModelAction::create_cv(ModelAction *parent) if (parent) cv = new ClockVector(parent->cv, this); else - cv = new ClockVector(); + cv = new ClockVector(NULL, this); } void ModelAction::read_from(ModelAction *act) diff --git a/clockvector.cc b/clockvector.cc index 367fa6e..f411f50 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -14,8 +14,6 @@ ClockVector::ClockVector(ClockVector *parent, ModelAction *act) memset(clock, 0, num_threads * sizeof(int)); if (parent) std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int)); - else - clock[0] = 1; if (act) clock[id_to_int(act->get_tid())] = act->get_seq_number();