cprover
|
#include <invariant_set_domain.h>
Public Member Functions | |
invariant_set_domaint () | |
bool | merge (const invariant_set_domaint &other, locationt from, locationt to) |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
virtual void | transform (locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final |
void | make_top () final |
void | make_bottom () final |
void | make_entry () final |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
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 |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Public Attributes | |
tvt | has_values |
invariant_sett | invariant_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 20 of file invariant_set_domain.h.
|
inline |
Definition at line 23 of file invariant_set_domain.h.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 67 of file invariant_set_domain.h.
References invariant_sett::make_false().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 73 of file invariant_set_domain.h.
References invariant_sett::make_true().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 61 of file invariant_set_domain.h.
References invariant_sett::make_true().
|
inline |
Definition at line 32 of file invariant_set_domain.h.
References invariant_set, tvt::is_false(), invariant_sett::make_union(), and tvt::unknown().
|
inlinefinalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 44 of file invariant_set_domain.h.
References tvt::is_known(), invariant_sett::output(), tvt::to_string(), and transform().
|
finalvirtual |
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().
Referenced by output().
tvt invariant_set_domaint::has_values |
Definition at line 27 of file invariant_set_domain.h.
invariant_sett invariant_set_domaint::invariant_set |
Definition at line 28 of file invariant_set_domain.h.
Referenced by merge(), and transform().