cprover
|
The interface offered by a domain, allows code to manipulate domains without knowing their exact type. More...
#include <ai_domain.h>
Public Types | |
typedef goto_programt::const_targett | locationt |
typedef ai_history_baset::trace_ptrt | trace_ptrt |
Public Member Functions | |
virtual | ~ai_domain_baset () |
virtual void | transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns) |
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... | |
virtual void | transform (const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns)=0 |
virtual void | output (std::ostream &, const ai_baset &, const namespacet &) 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 |
no states More... | |
virtual void | make_top ()=0 |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
virtual void | make_entry ()=0 |
Make this domain a reasonable entry-point state. More... | |
virtual bool | is_bottom () const =0 |
virtual bool | is_top () const =0 |
virtual bool | ai_simplify (exprt &condition, const namespacet &) 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... | |
Protected Member Functions | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More... | |
ai_domain_baset (const ai_domain_baset &old) | |
A copy constructor is part of the domain interface. More... | |
The interface offered by a domain, allows code to manipulate domains without knowing their exact type.
Derive from this to implement domains.
Definition at line 57 of file ai_domain.h.
Definition at line 76 of file ai_domain.h.
Definition at line 77 of file ai_domain.h.
|
inlineprotected |
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface.
Definition at line 62 of file ai_domain.h.
|
inlineprotected |
A copy constructor is part of the domain interface.
Definition at line 67 of file ai_domain.h.
|
inlinevirtual |
Definition at line 72 of file ai_domain.h.
|
inlinevirtual |
also add
bool merge(const T &b, locationt from, locationt to); or bool merge(const T &b, trace_ptrt from, trace_ptrt to);
This computes the join between "this" and "b". Return true if "this" has changed. In the usual case, "b" is the updated state after "from" and "this" is the state before "to".
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") This method allows an expression to be simplified / evaluated using the current state. It is used to evaluate assertions and in program simplification return true if unchanged
Reimplemented in interval_domaint, and constant_propagator_domaint.
Definition at line 167 of file ai_domain.h.
|
virtual |
Simplifies the expression but keeps it as an l-value.
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 42 of file ai_domain.cpp.
|
pure virtual |
|
pure virtual |
|
pure virtual |
|
pure virtual |
Make this domain a reasonable entry-point state.
Implemented in escape_domaint, uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, global_may_alias_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.
|
pure virtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implemented in uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.
|
inlinevirtual |
Reimplemented in constant_propagator_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, uninitialized_domaint, rd_range_domaint, and invariant_set_domaint.
Definition at line 126 of file ai_domain.h.
|
virtual |
Reimplemented in dep_graph_domaint.
Definition at line 16 of file ai_domain.cpp.
|
virtual |
Definition at line 25 of file ai_domain.cpp.
|
inlinevirtual |
Gives a Boolean condition that is true for all values represented by the domain.
This allows domains to be converted into program invariants.
Definition at line 178 of file ai_domain.h.
|
pure virtual |
Implemented in invariant_set_domaint, constant_propagator_domaint, uninitialized_domaint, rd_range_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, custom_bitvector_domaint, dep_graph_domaint, and is_threaded_domaint.
|
inlinevirtual |
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)
in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after
"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "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())
The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature
Definition at line 99 of file ai_domain.h.