func_inst_map(),
inst_list(),
entry_insts(),
- action_list_buffer(),
predicate_tree_position()
{
predicate_tree_entry = new Predicate(NULL, true);
predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
// memories that are reclaimed after each execution
+ action_list_buffer = new SnapList<action_list_t *>();
read_locations = new loc_set_t();
val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
inst->unset_location();
}
+ action_list_buffer = new SnapList<action_list_t *>();
read_locations = new loc_set_t();
val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
void incr_exit_count() { exit_count++; }
uint32_t get_exit_count() { return exit_count; }
- ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
+ SnapList<action_list_t *> * get_action_list_buffer() { return action_list_buffer; }
void add_to_val_loc_map(uint64_t val, void * loc);
void add_to_val_loc_map(value_set_t * values, void * loc);
bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act);
/* Store action_lists when calls to update_tree are deferred */
- ModelList<action_list_t *> action_list_buffer;
+ SnapList<action_list_t *> * action_list_buffer;
/* read_locations: set of locations read by this FuncNode
* val_loc_map: keep track of locations that have the same values written to;
FuncNode * func_node = func_nodes[func_id];
func_node->set_predicate_tree_position(tid, NULL);
func_node->reset_inst_act_map(tid);
- //func_node->clear_read_map(tid);
action_list_t * curr_act_list = func_act_lists->back();
*/
func_node->incr_exit_count();
if (func_node->get_exit_count() >= 2) {
- ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
+ SnapList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
while (action_list_buffer->size() > 0) {
action_list_t * act_list = action_list_buffer->back();
action_list_buffer->pop_back();