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.
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().
|
pure virtual |
|
pure virtual |
|
pure virtual |
|
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.
Referenced by ai_baset::output(), output_json(), and output_xml().
|
virtual |
Reimplemented in dep_graph_domaint.
Definition at line 24 of file ai.cpp.
References json(), and output().
Referenced by ai_baset::output_json().
|
virtual |
Definition at line 34 of file ai.cpp.
References xmlt::data, output(), and xml().
|
pure virtual |
Implemented in is_threaded_domaint.
Referenced by ai_baset::do_function_call(), and ai_baset::visit().