From: Brian Norris Date: Tue, 4 Dec 2012 02:23:22 +0000 (-0800) Subject: model: privatize a few interfaces X-Git-Tag: oopsla2013~477 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67e374f0a24b266f2ea81913770e89a4aac68ff3;p=model-checker.git model: privatize a few interfaces These functions were only public for ModelAction::read_from, which has now been internalized into ModelChecker. --- diff --git a/model.cc b/model.cc index 2f9ec63..8c88a05 100644 --- a/model.cc +++ b/model.cc @@ -1913,7 +1913,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, } /** - * A public interface for getting the release sequence head(s) with which a + * An interface for getting the release sequence head(s) with which a * given ModelAction must synchronize. This function only returns a non-empty * result when it can locate a release sequence head with certainty. Otherwise, * it may mark the internal state of the ModelChecker so that it will handle diff --git a/model.h b/model.h index 6bb4788..a2bbab2 100644 --- a/model.h +++ b/model.h @@ -118,14 +118,11 @@ public: 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); bool isfeasibleprefix() const; bool assert_bug(const char *msg); void assert_user_bug(const char *msg); - void set_bad_synchronization(); - const model_params params; Node * get_curr_node() const; @@ -139,6 +136,7 @@ private: bool mo_may_allow(const ModelAction * writer, const ModelAction *reader); bool has_asserted() const; void set_assert(); + void set_bad_synchronization(); bool promises_expired() const; void execute_sleep_set(); void wake_up_sleeping_actions(ModelAction * curr); @@ -180,6 +178,7 @@ private: void post_r_modification_order(ModelAction *curr, const ModelAction *rf); bool r_modification_order(ModelAction *curr, const ModelAction *rf); bool w_modification_order(ModelAction *curr); + void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads); bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const; bool resolve_release_sequences(void *location, work_queue_t *work_queue);