cprover
uninitialized_domaint Class Reference

#include <uninitialized_domain.h>

Inheritance diagram for uninitialized_domaint:
[legend]
Collaboration diagram for uninitialized_domaint:
[legend]

Public Types

typedef std::set< irep_idtuninitializedt
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Public Member Functions

 uninitialized_domaint ()
 
void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
 
void make_top () final
 
void make_bottom () final
 
void make_entry () final
 
bool merge (const uninitialized_domaint &other, locationt from, locationt to)
 
- Public Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
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

uninitializedt uninitialized
 

Private Member Functions

void assign (const exprt &lhs)
 

Private Attributes

tvt has_values
 

Detailed Description

Definition at line 21 of file uninitialized_domain.h.

Member Typedef Documentation

◆ uninitializedt

Definition at line 29 of file uninitialized_domain.h.

Constructor & Destructor Documentation

◆ uninitialized_domaint()

uninitialized_domaint::uninitialized_domaint ( )
inline

Definition at line 24 of file uninitialized_domain.h.

Member Function Documentation

◆ assign()

void uninitialized_domaint::assign ( const exprt lhs)
private

◆ make_bottom()

void uninitialized_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 49 of file uninitialized_domain.h.

References has_values, and uninitialized.

◆ make_entry()

void uninitialized_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 55 of file uninitialized_domain.h.

References make_top().

◆ make_top()

void uninitialized_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 43 of file uninitialized_domain.h.

References has_values, and uninitialized.

Referenced by make_entry().

◆ merge()

bool uninitialized_domaint::merge ( const uninitialized_domaint other,
locationt  from,
locationt  to 
)
Returns
returns true iff there is something new

Definition at line 79 of file uninitialized_domain.cpp.

References has_values, tvt::is_false(), uninitialized, and tvt::unknown().

◆ output()

void uninitialized_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
finalvirtual

Reimplemented from ai_domain_baset.

Definition at line 64 of file uninitialized_domain.cpp.

References has_values, tvt::is_known(), tvt::to_string(), and uninitialized.

◆ transform()

Member Data Documentation

◆ has_values

tvt uninitialized_domaint::has_values
private

Definition at line 67 of file uninitialized_domain.h.

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

◆ uninitialized

uninitializedt uninitialized_domaint::uninitialized

Definition at line 30 of file uninitialized_domain.h.

Referenced by assign(), make_bottom(), make_top(), merge(), output(), and transform().


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