projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
7da0378
)
Edits
author
weiyu
<weiyuluo1232@gmail.com>
Wed, 19 Feb 2020 00:06:36 +0000
(16:06 -0800)
committer
weiyu
<weiyuluo1232@gmail.com>
Wed, 19 Feb 2020 00:06:36 +0000
(16:06 -0800)
funcnode.cc
patch
|
blob
|
history
diff --git
a/funcnode.cc
b/funcnode.cc
index 952824ce5db2df7c5a00a9616dd81a954a776c4a..2b6e647aa395cc19758a8d915572a2c29d47ade5 100644
(file)
--- a/
funcnode.cc
+++ b/
funcnode.cc
@@
-219,9
+219,6
@@
void FuncNode::update_tree(ModelAction * act)
write_locations->add(loc);
history->update_loc_wr_func_nodes_map(loc, this);
}
write_locations->add(loc);
history->update_loc_wr_func_nodes_map(loc, this);
}
-
- // Do not process writes for now
- return;
}
if (act->is_read()) {
}
if (act->is_read()) {
@@
-242,6
+239,7
@@
void FuncNode::update_tree(ModelAction * act)
}
// update_inst_tree(&inst_list); TODO
}
// update_inst_tree(&inst_list); TODO
+
update_predicate_tree(act);
// print_predicate_tree();
update_predicate_tree(act);
// print_predicate_tree();
@@
-298,7
+296,6
@@
void FuncNode::update_predicate_tree(ModelAction * next_act)
bool amended;
while (true) {
FuncInst * next_inst = get_inst(next_act);
bool amended;
while (true) {
FuncInst * next_inst = get_inst(next_act);
- next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
Predicate * unset_predicate = NULL;
bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate);
Predicate * unset_predicate = NULL;
bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate);
@@
-340,12
+337,13
@@
void FuncNode::update_predicate_tree(ModelAction * next_act)
continue;
}
continue;
}
- if (next_act->is_write())
+ if (next_act->is_write())
{
curr_pred->set_write(true);
curr_pred->set_write(true);
+ }
if (next_act->is_read()) {
/* Only need to store the locations of read actions */
if (next_act->is_read()) {
/* Only need to store the locations of read actions */
- loc_inst_map->put(next_
ins
t->get_location(), next_inst);
+ loc_inst_map->put(next_
ac
t->get_location(), next_inst);
}
inst_pred_map->put(next_inst, curr_pred);
}
inst_pred_map->put(next_inst, curr_pred);
@@
-356,12
+354,17
@@
void FuncNode::update_predicate_tree(ModelAction * next_act)
curr_pred->incr_expl_count();
add_predicate_to_trace(tid, curr_pred);
curr_pred->incr_expl_count();
add_predicate_to_trace(tid, curr_pred);
+ if (next_act->is_read())
+ next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
+
break;
}
// A check
break;
}
// A check
- if (selected_branch != NULL && !amended)
- ASSERT(selected_branch == curr_pred);
+ if (next_act->is_read()) {
+ if (selected_branch != NULL && !amended)
+ ASSERT(selected_branch == curr_pred);
+ }
}
/* Given curr_pred and next_inst, find the branch following curr_pred that
}
/* Given curr_pred and next_inst, find the branch following curr_pred that
@@
-413,7
+416,6
@@
bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
case EQUALITY:
FuncInst * to_be_compared;
to_be_compared = pred_expression->func_inst;
case EQUALITY:
FuncInst * to_be_compared;
to_be_compared = pred_expression->func_inst;
- ASSERT(to_be_compared != next_inst);
last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
ASSERT(last_read != VALUE_NONE);
last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
ASSERT(last_read != VALUE_NONE);