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 | is_bottom () const =0 |
virtual bool | is_top () const =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 113 of file ai.h.
Referenced by ai_simplify_lhs(), static_simplifier(), and static_verifier().
|
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 static_simplifier().
|
pure virtual |
|
pure virtual |
|
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, constant_propagator_domaint, and custom_bitvector_domaint.
Definition at line 67 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 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 ai_baset::do_function_call(), and ai_baset::visit().