remove STL vector

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index cfbc3b8606243e1cf558a1e7a2a48d0bd3c70967..78729bd38ac4d9da05d25527450f6668f38be997 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -41,6 +41,9 @@ ModelChecker::ModelChecker() :
 {
        memset(&stats,0,sizeof(struct execution_stats));
        init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);    // L: user_main_wrapper passes the user program
+#ifdef TLS
+       init_thread->setTLS((char *)get_tls_addr());
+#endif
        execution->add_thread(init_thread);
        scheduler->set_current_thread(init_thread);
        execution->setParams(&params);
@@ -139,28 +142,6 @@ bool ModelChecker::assert_bug(const char *msg, ...)
        return execution->assert_bug(str);
 }
 
-/**
- * @brief Assert a data race in the executing program.
- *
- * Different from assert_bug, the program will not be aborted immediately
- * upon calling this function, unless the number of data races exceeds
- * a threshold.
- *
- * @param msg Descriptive message for the bug (do not include newline char)
- * @return True if bug is immediately-feasible
- */
-bool ModelChecker::assert_race(const char *msg, ...)
-{
-       char str[800];
-
-       va_list ap;
-       va_start(ap, msg);
-       vsnprintf(str, sizeof(str), msg, ap);
-       va_end(ap);
-
-       return execution->assert_race(str);
-}
-
 /**
  * @brief Assert a bug in the executing program, asserted by a user thread
  * @see ModelChecker::assert_bug
@@ -338,11 +319,11 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
-       if (forklock) {
+       if (modellock) {
                static bool fork_message_printed = false;
 
                if (!fork_message_printed) {
-                       model_print("Fork handler trying to call into model checker...\n");
+                       model_print("Fork handler or dead thread trying to call into model checker...\n");
                        fork_message_printed = true;
                }
                delete act;
@@ -372,6 +353,8 @@ static void runChecker() {
 
 void ModelChecker::startChecker() {
        startExecution(get_system_context(), runChecker);
+       snapshot_stack_init();
+       snapshot_record(0);
 }
 
 bool ModelChecker::should_terminate_execution()
@@ -382,6 +365,8 @@ bool ModelChecker::should_terminate_execution()
        else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
                execution->set_assert();
                return true;
+       } else if (execution->isFinished()) {
+               return true;
        }
        return false;
 }
@@ -404,7 +389,7 @@ void ModelChecker::do_restart()
 void ModelChecker::startMainThread() {
        init_thread->set_state(THREAD_RUNNING);
        scheduler->set_current_thread(init_thread);
-       thread_startup();
+       main_thread_startup();
 }
 
 static bool is_nonsc_write(const ModelAction *act) {