Checking whether every write in the rf_set satisfies read modification order does...

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index 05974d781ad52bfac0445b3dcaeb98dfabcd990d..c739a284a0d4b0c7aaac36cd54eb480576714d73 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -20,12 +20,13 @@ FuncNode::FuncNode(ModelHistory * history) :
 {
        predicate_tree_entry = new Predicate(NULL, true);
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+       predicate_tree_exit = new Predicate(NULL, false, true);
 
-       // Memories that are reclaimed after each execution
+       /* Snapshot data structures below */
        action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
-       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
 
        //values_may_read_from = new value_set_t();
@@ -37,7 +38,7 @@ void FuncNode::set_new_exec_flag()
        action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
-       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+       val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
 
        //values_may_read_from = new value_set_t();
@@ -281,7 +282,6 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 
                                curr_pred->add_backedge(back_pred);
                                curr_pred = back_pred;
-
                                continue;
                        }
                }
@@ -306,7 +306,10 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        inst_id_map.put(next_inst, inst_counter++);
 
                it = it->getNext();
+               /*-- curr_pred->incr_expl_count(); */
        }
+
+       curr_pred->set_exit(predicate_tree_exit);
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
@@ -695,6 +698,7 @@ void FuncNode::print_predicate_tree()
 {
        model_print("digraph function_%s {\n", func_name);
        predicate_tree_entry->print_pred_subtree();
+       predicate_tree_exit->print_predicate();
        model_print("}\n");     // end of graph
 }