From: Brian Norris <banorris@uci.edu>
Date: Sun, 4 Nov 2012 00:50:26 +0000 (-0700)
Subject: common: early quit on MODEL_ASSERT()
X-Git-Tag: pldi2013~14
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=ddea30a10d1acaef02712575c6fa4856de72cd4c;hp=d596a0e422232c82e01fe266ca2099d0eff5de0f

common: early quit on MODEL_ASSERT()

If a user program hits an assertion, we should quit before executing any
further. i.e., don't even wait for the next atomic action, since the
assertion might trigger more bugs that have unintended/unforseen
consequences.
---

diff --git a/common.cc b/common.cc
index 20102b0..f4aa7ec 100644
--- a/common.cc
+++ b/common.cc
@@ -49,5 +49,6 @@ void model_assert(bool expr, const char *file, int line)
 		printf("  [BUG] Program has hit assertion in file %s at line %d\n",
 				file, line);
 		model->set_assert();
+		model->switch_to_master(NULL);
 	}
 }