cprover
|
#include <invariant_set_domain.h>
Public Member Functions | |
invariant_set_domaint () | |
bool | merge (const invariant_set_domaint &other, locationt, locationt) |
void | output (std::ostream &out, const ai_baset &, const namespacet &) const final override |
virtual void | transform (locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final override |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More... | |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
void | make_bottom () final override |
no states More... | |
void | make_entry () final override |
a reasonable entry-point state More... | |
bool | is_top () const override final |
bool | is_bottom () const override final |
![]() | |
virtual | ~ai_domain_baset () |
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const |
also add More... | |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Simplifies the expression but keeps it as an l-value. More... | |
virtual exprt | to_predicate (void) const |
Gives a Boolean condition that is true for all values represented by the domain. More... | |
Public Attributes | |
tvt | has_values |
invariant_sett | invariant_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
Definition at line 20 of file invariant_set_domain.h.
|
inline |
Definition at line 23 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 84 of file invariant_set_domain.h.
References has_values, and tvt::is_false().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 79 of file invariant_set_domain.h.
References has_values, and tvt::is_true().
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 67 of file invariant_set_domain.h.
References has_values, invariant_set, and invariant_sett::make_false().
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 73 of file invariant_set_domain.h.
References has_values, invariant_set, and invariant_sett::make_true().
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 61 of file invariant_set_domain.h.
References has_values, invariant_set, and invariant_sett::make_true().
|
inline |
Definition at line 32 of file invariant_set_domain.h.
References has_values, invariant_set, tvt::is_false(), invariant_sett::make_union(), and tvt::unknown().
|
inlinefinaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 44 of file invariant_set_domain.h.
References has_values, invariant_set, tvt::is_known(), invariant_sett::output(), and tvt::to_string().
|
finaloverridevirtual |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
Implements ai_domain_baset.
Definition at line 16 of file invariant_set_domain.cpp.
References invariant_sett::apply_code(), ASSERT, ASSIGN, invariant_sett::assignment(), ASSUME, DECL, FUNCTION_CALL, GOTO, invariant_set, code_assignt::lhs(), exprt::make_not(), invariant_sett::make_threaded(), OTHER, RETURN, code_assignt::rhs(), simplify(), START_THREAD, invariant_sett::strengthen(), and to_code_assign().
tvt invariant_set_domaint::has_values |
Definition at line 27 of file invariant_set_domain.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and output().
invariant_sett invariant_set_domaint::invariant_set |
Definition at line 28 of file invariant_set_domain.h.
Referenced by make_bottom(), make_entry(), make_top(), merge(), output(), and transform().