cprover
Public Member Functions | Public Attributes | List of all members
is_threaded_domaint Class Reference
Inheritance diagram for is_threaded_domaint:
[legend]
Collaboration diagram for is_threaded_domaint:
[legend]

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
 
- Public Member Functions inherited from ai_domain_baset
 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

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Detailed Description

Definition at line 18 of file is_threaded.cpp.

Constructor & Destructor Documentation

◆ is_threaded_domaint()

is_threaded_domaint::is_threaded_domaint ( )
inline

Definition at line 24 of file is_threaded.cpp.

Member Function Documentation

◆ make_bottom()

void is_threaded_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 66 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ make_entry()

void is_threaded_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 78 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ make_top()

void is_threaded_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 72 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ merge()

bool is_threaded_domaint::merge ( const is_threaded_domaint &  src,
locationt  from,
locationt  to 
)
inline

Definition at line 31 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ transform()

void is_threaded_domaint::transform ( locationt  from,
locationt  to,
ai_baset &  ai,
const namespacet &  ns 
)
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 51 of file is_threaded.cpp.

References is_threaded, and reachable.

Member Data Documentation

◆ is_threaded

bool is_threaded_domaint::is_threaded

Definition at line 22 of file is_threaded.cpp.

Referenced by make_bottom(), make_entry(), make_top(), merge(), and transform().

◆ reachable

bool is_threaded_domaint::reachable

Definition at line 21 of file is_threaded.cpp.

Referenced by make_bottom(), make_entry(), make_top(), merge(), and transform().

The documentation for this class was generated from the following file: