Method revisit

src/FunctionInvocationUser.cpp:319–371

* return true if the invocation is valid (not violating fixed facts), false other wise * * side effects: update input facts and FactMgr in cg_context if the invocation is found valid */

 * side effects: update input facts and FactMgr in cg_context if the invocation is found valid
 */
bool
FunctionInvocationUser::revisit(std::vector<const Fact*>& inputs, CGContext& cg_context) const
{
	FactMgr* fm = get_fact_mgr_for_func(func);
	fm->clear_map_visited();
	if (func->visited_cnt++ == 0) {
		fm->setup_in_out_maps(true);
	}
	// for debugging
	if (func->name=="func_10" && func->visited_cnt==19) {
		//cout << func->visited_cnt << endl;
		//func->Output(cout);
		//cout << endl;
	}

	// make copies so we can back up if fail
	vector<const Fact*> inputs_copy = inputs;

	// add facts related to pass parameters
	fm->caller_to_callee_handover(this, inputs);

	map<const Statement*, FactVec> facts_in_copy = fm->map_facts_in;
	map<const Statement*, FactVec> facts_out_copy = fm->map_facts_out;
	map<const Statement*, Effect>  stm_effect_copy = fm->map_stm_effect;
	map<const Statement*, Effect>  accum_effect_copy = fm->map_accum_effect;
	// TODO: revisit only if "contingent variable" has been changed?
	if (!func->body->visit_facts(inputs, cg_context)) {
		// restore facts and effect
		fm->map_facts_in = facts_in_copy;
		fm->map_facts_out = facts_out_copy;
		fm->map_stm_effect = stm_effect_copy;
		fm->map_accum_effect = accum_effect_copy;
		inputs = inputs_copy;
		return false;
	}
	cg_context.add_effect(fm->map_stm_effect[func->body]);
	FactVec ret_facts;
	func->body->add_back_return_facts(fm, ret_facts);
	save_return_fact(ret_facts);
	// incorporate early return facts
	merge_facts(inputs, ret_facts);

	// remove facts related to passing parameters
	FactMgr::update_facts_for_oos_vars(func->param, inputs);

	fm->setup_in_out_maps(false);
	// remember the effect context during this visit to this function
	func->accum_eff_context.add_external_effect(cg_context.get_effect_context());
	// update the original facts with new facts changed by function call
	renew_facts(inputs_copy, inputs);
	inputs = inputs_copy;
	return true;
}

/*
 * save the return fact for later use