From: Brian Norris Date: Thu, 13 Sep 2012 17:16:37 +0000 (-0700) Subject: model: simple ASSERT() bug X-Git-Tag: pldi2013~204 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1d5bf75a20115d8c73b44825f09aab705afce301;p=model-checker.git model: simple ASSERT() bug Don't ASSERT(rf->is_write()) until we're sure that rf is non-NULL. --- diff --git a/model.cc b/model.cc index 4475455..b566b62 100644 --- a/model.cc +++ b/model.cc @@ -781,11 +781,13 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con bool ModelChecker::release_seq_head(const ModelAction *rf, std::vector *release_heads) const { - ASSERT(rf->is_write()); if (!rf) { /* read from future: need to settle this later */ return false; /* incomplete */ } + + ASSERT(rf->is_write()); + if (rf->is_release()) release_heads->push_back(rf); if (rf->is_rmw()) {