cprover
|
Public Member Functions | |
is_threaded_domaint () | |
bool | merge (const is_threaded_domaint &src, locationt from, locationt to) |
void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final |
void | make_bottom () final |
void | make_top () final |
void | make_entry () final |
![]() | |
ai_domain_baset () | |
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 |
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... | |
Public Attributes | |
bool | reachable |
bool | is_threaded |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 18 of file is_threaded.cpp.
|
inline |
Definition at line 24 of file is_threaded.cpp.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 66 of file is_threaded.cpp.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 78 of file is_threaded.cpp.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 72 of file is_threaded.cpp.
|
inline |
Definition at line 31 of file is_threaded.cpp.
References is_threaded, and reachable.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 51 of file is_threaded.cpp.
bool is_threaded_domaint::is_threaded |
Definition at line 22 of file is_threaded.cpp.
Referenced by is_threadedt::compute(), and merge().
bool is_threaded_domaint::reachable |
Definition at line 21 of file is_threaded.cpp.
Referenced by merge().