cprover
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, 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
 
- Public Member Functions inherited from 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
 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
 
- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. 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 78 of file is_threaded.cpp.

References DATA_INVARIANT, is_threaded, and reachable.

◆ is_top()

bool is_threaded_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 86 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ make_bottom()

void is_threaded_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 60 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ make_entry()

void is_threaded_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 72 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ 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 66 of file is_threaded.cpp.

References is_threaded, and reachable.

◆ merge()

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

Definition at line 31 of file is_threaded.cpp.

References INVARIANT, is_threaded, and reachable.

◆ transform()

void is_threaded_domaint::transform ( locationt  from,
locationt  to,
ai_baset ai,
const namespacet ns 
)
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.

Member Data Documentation

◆ is_threaded

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().

◆ reachable

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().


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