cprover
|
Public Member Functions | |
is_threaded_domaint () | |
bool | merge (const is_threaded_domaint &src, locationt, locationt) |
void | transform (locationt from, locationt, ai_baset &, const namespacet &) final override |
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... | |
void | make_bottom () final override |
no states More... | |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
void | make_entry () final override |
a reasonable entry-point state More... | |
bool | is_bottom () const override final |
bool | is_top () const override final |
![]() | |
virtual | ~ai_domain_baset () |
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 bool | ai_simplify (exprt &condition, const namespacet &ns) 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 | |
bool | reachable |
bool | is_threaded |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
Definition at line 18 of file is_threaded.cpp.
|
inline |
Definition at line 24 of file is_threaded.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 78 of file is_threaded.cpp.
References DATA_INVARIANT, is_threaded, and reachable.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 86 of file is_threaded.cpp.
References is_threaded, and reachable.
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 60 of file is_threaded.cpp.
References is_threaded, and reachable.
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 72 of file is_threaded.cpp.
References is_threaded, and reachable.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 66 of file is_threaded.cpp.
References is_threaded, and reachable.
|
inline |
Definition at line 31 of file is_threaded.cpp.
References INVARIANT, is_threaded, and reachable.
|
inlinefinaloverridevirtual |
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)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "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())
Implements ai_domain_baset.
Definition at line 50 of file is_threaded.cpp.
References INVARIANT, is_threaded, and reachable.
bool is_threaded_domaint::is_threaded |
Definition at line 22 of file is_threaded.cpp.
Referenced by is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and transform().
bool is_threaded_domaint::reachable |
Definition at line 21 of file is_threaded.cpp.
Referenced by is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and transform().