annoying bug... Optimization was originally intended for the following insight:

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index d0043a1f88b1990de8e0fcdee27e21baa387ccd7..59a07597bb5bf0436752ad6a4fca2f22d9fa2fe8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -99,6 +99,7 @@ public:
        bool isfeasible();
        bool isfeasibleotherthanRMW();
        bool isfinalfeasible();
+       void check_promises_thread_disabled();
        void mo_check_promises(thread_id_t tid, const ModelAction *write);
        void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
        void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
@@ -139,7 +140,7 @@ private:
         */
        void set_current_action(ModelAction *act) { priv->current_action = act; }
        Thread * check_current_action(ModelAction *curr);
-       ModelAction * initialize_curr_action(ModelAction *curr);
+       bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);
        bool process_mutex(ModelAction *curr);