cprover
|
#include <ai.h>
Public Types | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
virtual void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const |
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 void | make_bottom ()=0 |
virtual void | make_top ()=0 |
virtual void | make_entry ()=0 |
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... | |
|
inlinevirtual |
Reimplemented in interval_domaint, and constant_propagator_domaint.
Definition at line 93 of file ai.h.
References ai_simplify_lhs().
Referenced by ai_simplify_lhs().
|
virtual |
Use the information in the domain to simplify the expression on the LHS of an assignment.
This for example won't simplify symbols to their values, but does simplify indices in arrays, members of structs and dereferencing of pointers
condition | the expression to simplify |
ns | the namespace |
Definition at line 53 of file ai.cpp.
References ai_simplify(), member_exprt::compound(), irept::id(), index_exprt::index(), dereference_exprt::pointer(), simplify_expr(), to_dereference_expr(), to_index_expr(), and to_member_expr().
Referenced by ai_simplify().
|
pure virtual |
Implemented in rd_range_domaint, dep_graph_domaint, invariant_set_domaint, is_threaded_domaint, interval_domaint, uninitialized_domaint, escape_domaint, global_may_alias_domaint, custom_bitvector_domaint, and constant_propagator_domaint.
Referenced by output().
|
pure virtual |
Implemented in rd_range_domaint, dep_graph_domaint, is_threaded_domaint, interval_domaint, invariant_set_domaint, escape_domaint, global_may_alias_domaint, uninitialized_domaint, custom_bitvector_domaint, and constant_propagator_domaint.
Referenced by ai_baset::entry_state(), and output().
|
pure virtual |
Implemented in rd_range_domaint, dep_graph_domaint, is_threaded_domaint, interval_domaint, invariant_set_domaint, escape_domaint, global_may_alias_domaint, custom_bitvector_domaint, uninitialized_domaint, and constant_propagator_domaint.
Referenced by output().
|
inlinevirtual |
Reimplemented in rd_range_domaint, dep_graph_domaint, invariant_set_domaint, interval_domaint, uninitialized_domaint, escape_domaint, global_may_alias_domaint, custom_bitvector_domaint, and constant_propagator_domaint.
Definition at line 56 of file ai.h.
References make_bottom(), make_entry(), make_top(), output_json(), and output_xml().
Referenced by ai_baset::clear(), ai_baset::output(), output_json(), output_xml(), and ai_baset::output_xml().
|
virtual |
Reimplemented in dep_graph_domaint.
Definition at line 24 of file ai.cpp.
References json(), and output().
Referenced by output(), ai_baset::output(), ai_baset::output_json(), and ai_baset::output_xml().
|
virtual |
Definition at line 34 of file ai.cpp.
References xmlt::data, output(), and xml().
Referenced by output(), ai_baset::output_json(), and ai_baset::output_xml().
|
pure virtual |
Implemented in is_threaded_domaint.
Referenced by ai_baset::visit().