Go to the documentation of this file.
24 : options(options), ui_message_handler(ui_message_handler), equation(equation)
39 conjuncts.push_back(inst->cond_handle);
48 for(symex_target_equationt::SSA_stepst::iterator it =
55 irep_idt property_id = it->get_property_id();
59 auto property_pair_it = properties.find(property_id);
61 property_pair_it != properties.end() &&
66 goal_map[property_id].instances.push_back(it);
78 goal_pair.second.condition =
solver->decision_procedure().handle(
84 std::function<
bool(
const irep_idt &)> select_property)
88 for(
const auto &goal_pair :
goal_map)
91 select_property(goal_pair.first) &&
92 !goal_pair.second.condition.is_false())
94 disjuncts.push_back(goal_pair.second.condition);
104 return solver->decision_procedure()();
110 return solver->decision_procedure();
116 return solver->stack_decision_procedure();
126 std::unordered_set<irep_idt> &updated_properties,
135 auto &status = properties.at(goal_pair.first).status;
137 solver->decision_procedure()
138 .get(goal_pair.second.condition)
143 updated_properties.insert(goal_pair.first);
151 for(
auto &property_pair : properties)
156 updated_properties.insert(property_pair.first);
161 for(
auto &property_pair : properties)
166 updated_properties.insert(property_pair.first);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
@ FAIL
The property was violated.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
@ ERROR
An error occurred during goto checking.
#define CHECK_RETURN(CONDITION)
ui_message_handlert & ui_message_handler
std::unique_ptr< solver_factoryt::solvert > solver
Property Decider for Goto-Symex.
Base class for all expressions.
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
symex_target_equationt & get_equation() const
Return the equation associated with this instance.
virtual uit get_ui() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
symex_target_equationt & equation
goto_symex_property_decidert(const optionst &options, ui_message_handlert &ui_message_handler, symex_target_equationt &equation, const namespacet &ns)
void convert_goals()
Convert the instances of a property into a goal variable.
std::map< irep_idt, goalt > goal_map
Maintains the relation between a property ID and the corresponding goal variable that encodes the neg...
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
std::vector< exprt > operandst
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
resultt
Result of running the decision procedure.
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
@ UNKNOWN
The checker was unable to determine the status of the property.
void update_properties_goals_from_symex_target_equation(propertiest &properties)
Get the conditions for the properties from the equation and collect all 'instances' of the properties...
std::vector< symex_target_equationt::SSA_stepst::iterator > instances
A property holds if all instances of it are true.
void update_properties_status_from_goals(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const
Update the property status from the truth value of the goal variable.
@ PASS
The property was not violated.