cprover
is_threaded_domaint Class Reference
+ Inheritance diagram for is_threaded_domaint:
+ Collaboration diagram for is_threaded_domaint:

Public Member Functions

 is_threaded_domaint ()
 
bool merge (const is_threaded_domaint &src, locationt, locationt)
 
void transform (const irep_idt &, locationt from, const irep_idt &, locationt, ai_baset &, const namespacet &) final override
 
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
 Make this domain a reasonable entry-point state. More...
 
bool is_bottom () const override final
 
bool is_top () const override final
 
- Public Member Functions inherited from ai_domain_baset
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 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 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

bool reachable
 
bool is_threaded
 

Additional Inherited Members

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 
- Protected Member Functions inherited from ai_domain_baset
 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...
 

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

◆ is_bottom()

bool is_threaded_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 82 of file is_threaded.cpp.

◆ is_top()

bool is_threaded_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 90 of file is_threaded.cpp.

◆ make_bottom()

void is_threaded_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 64 of file is_threaded.cpp.

◆ make_entry()

void is_threaded_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 76 of file is_threaded.cpp.

◆ make_top()

void is_threaded_domaint::make_top ( )
inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 70 of file is_threaded.cpp.

◆ merge()

bool is_threaded_domaint::merge ( const is_threaded_domaint src,
locationt  ,
locationt   
)
inline

Definition at line 31 of file is_threaded.cpp.

◆ transform()

void is_threaded_domaint::transform ( const irep_idt function_from,
locationt  from,
const irep_idt function_to,
locationt  to,
ai_baset ai,
const namespacet ns 
)
inlinefinaloverridevirtual
Deprecated:
SINCE(2019, 08, 01, "use the history signature instead")

Implements ai_domain_baset.

Definition at line 49 of file is_threaded.cpp.

Member Data Documentation

◆ is_threaded

bool is_threaded_domaint::is_threaded

Definition at line 22 of file is_threaded.cpp.

◆ reachable

bool is_threaded_domaint::reachable

Definition at line 21 of file is_threaded.cpp.


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