#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
*/
user_main(model->params.argc, model->params.argv);
}
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+ return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
return true;
}
- if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ if (too_many_steps())
return true;
return false;
}