cprover
constant_propagator_domaint::valuest Struct Reference

#include <constant_propagator.h>

Collaboration diagram for constant_propagator_domaint::valuest:
[legend]

Public Member Functions

bool merge (const valuest &src)
 join More...
 
bool meet (const valuest &src, const namespacet &ns)
 meet More...
 
void set_to_bottom ()
 
void set_to_top ()
 
bool is_bot () const
 
bool is_top () const
 
void set_to (const irep_idt &lhs, const exprt &rhs)
 
void set_to (const symbol_exprt &lhs, const exprt &rhs)
 
bool set_to_top (const symbol_exprt &expr)
 
bool set_to_top (const irep_idt &id)
 Do not call this when iterating over replace_const.expr_map! More...
 
void set_dirty_to_top (const dirtyt &dirty, const namespacet &ns)
 
bool is_constant (const exprt &expr) const
 
bool is_array_constant (const exprt &expr) const
 
bool is_constant_address_of (const exprt &expr) const
 
bool is_empty () const
 
void output (std::ostream &out, const namespacet &ns) const
 

Public Attributes

replace_symbolt replace_const
 
bool is_bottom = true
 

Detailed Description

Definition at line 71 of file constant_propagator.h.

Member Function Documentation

◆ is_array_constant()

bool constant_propagator_domaint::valuest::is_array_constant ( const exprt expr) const

◆ is_bot()

bool constant_propagator_domaint::valuest::is_bot ( ) const
inline

◆ is_constant()

◆ is_constant_address_of()

bool constant_propagator_domaint::valuest::is_constant_address_of ( const exprt expr) const

◆ is_empty()

bool constant_propagator_domaint::valuest::is_empty ( ) const
inline

Definition at line 130 of file constant_propagator.h.

References replace_symbolt::expr_map, and replace_const.

◆ is_top()

bool constant_propagator_domaint::valuest::is_top ( ) const
inline

◆ meet()

bool constant_propagator_domaint::valuest::meet ( const valuest src,
const namespacet ns 
)

◆ merge()

bool constant_propagator_domaint::valuest::merge ( const valuest src)

join

Returns
Return true if "this" has changed.

Definition at line 408 of file constant_propagator.cpp.

References replace_symbolt::expr_map, irept::find(), INVARIANT, constant_propagator_domaint::is_bottom(), is_bottom, PRECONDITION, and replace_const.

Referenced by constant_propagator_domaint::merge().

◆ output()

void constant_propagator_domaint::valuest::output ( std::ostream &  out,
const namespacet ns 
) const

◆ set_dirty_to_top()

void constant_propagator_domaint::valuest::set_dirty_to_top ( const dirtyt dirty,
const namespacet ns 
)

◆ set_to() [1/2]

void constant_propagator_domaint::valuest::set_to ( const irep_idt lhs,
const exprt rhs 
)
inline

◆ set_to() [2/2]

void constant_propagator_domaint::valuest::set_to ( const symbol_exprt lhs,
const exprt rhs 
)
inline

Definition at line 112 of file constant_propagator.h.

References symbol_exprt::get_identifier(), and set_to().

◆ set_to_bottom()

void constant_propagator_domaint::valuest::set_to_bottom ( )
inline

◆ set_to_top() [1/3]

void constant_propagator_domaint::valuest::set_to_top ( )
inline

◆ set_to_top() [2/3]

bool constant_propagator_domaint::valuest::set_to_top ( const symbol_exprt expr)
inline

Definition at line 117 of file constant_propagator.h.

References symbol_exprt::get_identifier(), and set_to_top().

◆ set_to_top() [3/3]

bool constant_propagator_domaint::valuest::set_to_top ( const irep_idt id)

Do not call this when iterating over replace_const.expr_map!

Definition at line 338 of file constant_propagator.cpp.

References INVARIANT, constant_propagator_domaint::is_bottom(), and size_type().

Member Data Documentation

◆ is_bottom

bool constant_propagator_domaint::valuest::is_bottom = true

◆ replace_const


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