model: remove unnecessary DEBUG()

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 33fc4c3c38c3b5affc65bf360a833f5de8f8175e..3ed8203fe9a2111618ced00d3ac07bf0cc5a6ac1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -56,7 +56,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        bad_synchronization(false)
 {
        /* Allocate this "size" on the snapshotting heap */
-       priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
+       priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
        /* First thread created will have id INITIAL_THREAD_ID */
        priv->next_thread_id = INITIAL_THREAD_ID;
 
@@ -88,6 +88,8 @@ ModelChecker::~ModelChecker()
        delete node_stack;
        delete scheduler;
        delete mo_graph;
+
+       snapshot_free(priv);
 }
 
 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
@@ -335,9 +337,6 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
        }
 
-       DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
-                       pending_rel_seqs->size());
-
 
        if (isfinalfeasible() || DBG_ENABLED()) {
                checkDataRaces();
@@ -1038,7 +1037,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        }
 }
 
-bool ModelChecker::promises_expired() {
+bool ModelChecker::promises_expired() const
+{
        for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
                Promise *promise = (*promises)[promise_index];
                if (promise->get_expiration()<priv->used_sequence_numbers) {
@@ -1050,12 +1050,14 @@ bool ModelChecker::promises_expired() {
 
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
+bool ModelChecker::isfeasibleprefix() const
+{
        return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+bool ModelChecker::isfeasible() const
+{
        if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
                DEBUG("Infeasible: RMW violation\n");
 
@@ -1064,7 +1066,8 @@ bool ModelChecker::isfeasible() {
 
 /** @return whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+bool ModelChecker::isfeasibleotherthanRMW() const
+{
        if (DBG_ENABLED()) {
                if (mo_graph->checkForCycles())
                        DEBUG("Infeasible: modification order cycles\n");
@@ -1081,7 +1084,8 @@ bool ModelChecker::isfeasibleotherthanRMW() {
 }
 
 /** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
+bool ModelChecker::isfinalfeasible() const
+{
        if (DBG_ENABLED() && promises->size() != 0)
                DEBUG("Infeasible: unrevolved promises\n");