X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=826497945556055254e7ef8a0a32507fc7bc4716;hb=53a04a6ac7cbbf37880effe033704143bd6aaaaf;hp=eed548cc0c906b0d50b6c78f89e51e15aa4b4e1b;hpb=56596a27332a3622b935d5b75f81f4773dcbf757;p=model-checker.git

diff --git a/model.cc b/model.cc
index eed548c..8264979 100644
--- a/model.cc
+++ b/model.cc
@@ -17,25 +17,12 @@
 #include "threads-model.h"
 #include "output.h"
 #include "traceanalysis.h"
+#include "bugmessage.h"
 
 #define INITIAL_THREAD_ID	0
 
 ModelChecker *model;
 
-struct bug_message {
-	bug_message(const char *str) {
-		const char *fmt = "  [BUG] %s\n";
-		msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
-		sprintf(msg, fmt, str);
-	}
-	~bug_message() { if (msg) snapshot_free(msg); }
-
-	char *msg;
-	void print() { model_print("%s", msg); }
-
-	SNAPSHOTALLOC
-};
-
 /**
  * Structure for holding small ModelChecker members that should be snapshotted
  */