cprover
|
#include <invariant_set_domain.h>
Public Member Functions | |
invariant_set_domaint (value_setst &value_sets, inv_object_storet &object_store, const namespacet &ns) | |
bool | merge (const invariant_set_domaint &other, locationt, locationt) |
void | output (std::ostream &out, const ai_baset &, const namespacet &) const final override |
virtual void | transform (const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l, ai_baset &ai, const namespacet &ns) final override |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
void | make_bottom () final override |
no states More... | |
void | make_entry () final override |
Make this domain a reasonable entry-point state. More... | |
bool | is_top () const override final |
bool | is_bottom () const override final |
![]() | |
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 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 &) 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... | |
Public Attributes | |
tvt | has_values |
invariant_sett | invariant_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef ai_history_baset::trace_ptrt | trace_ptrt |
![]() | |
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... | |
Definition at line 20 of file invariant_set_domain.h.
|
inline |
Definition at line 23 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 90 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 85 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 79 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 67 of file invariant_set_domain.h.
|
inline |
Definition at line 36 of file invariant_set_domain.h.
|
inlinefinaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 48 of file invariant_set_domain.h.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 17 of file invariant_set_domain.cpp.
tvt invariant_set_domaint::has_values |
Definition at line 31 of file invariant_set_domain.h.
invariant_sett invariant_set_domaint::invariant_set |
Definition at line 32 of file invariant_set_domain.h.