CBMC
Public Member Functions | Public Attributes | List of all members
constant_propagator_domaint::valuest Struct Reference

#include <constant_propagator.h>

+ Collaboration diagram for constant_propagator_domaint::valuest:

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 symbol_exprt &lhs, const exprt &rhs)
 
bool set_to_top (const symbol_exprt &expr)
 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 namespacet &ns) const
 
bool is_constant (const irep_idt &id, const namespacet &ns) const
 
bool is_empty () const
 
void output (std::ostream &out, const namespacet &ns) const
 

Public Attributes

address_of_aware_replace_symbolt replace_const
 
bool is_bottom = true
 

Detailed Description

Definition at line 78 of file constant_propagator.h.

Member Function Documentation

◆ is_bot()

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

Definition at line 101 of file constant_propagator.h.

◆ is_constant() [1/2]

bool constant_propagator_domaint::valuest::is_constant ( const exprt &  expr,
const namespacet &  ns 
) const

Definition at line 446 of file constant_propagator.cpp.

◆ is_constant() [2/2]

bool constant_propagator_domaint::valuest::is_constant ( const irep_idt &  id,
const namespacet &  ns 
) const

Definition at line 453 of file constant_propagator.cpp.

◆ is_empty()

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

Definition at line 125 of file constant_propagator.h.

◆ is_top()

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

Definition at line 106 of file constant_propagator.h.

◆ meet()

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

meet

Returns
Return true if "this" has changed.

Definition at line 606 of file constant_propagator.cpp.

◆ merge()

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

join

Returns
Return true if "this" has changed.

Definition at line 535 of file constant_propagator.cpp.

◆ output()

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

Definition at line 498 of file constant_propagator.cpp.

◆ set_dirty_to_top()

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

Definition at line 473 of file constant_propagator.cpp.

◆ set_to()

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

Definition at line 111 of file constant_propagator.h.

◆ set_to_bottom()

void constant_propagator_domaint::valuest::set_to_bottom ( )
inline

Definition at line 89 of file constant_propagator.h.

◆ set_to_top() [1/2]

void constant_propagator_domaint::valuest::set_to_top ( )
inline

Definition at line 95 of file constant_propagator.h.

◆ set_to_top() [2/2]

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

Do not call this when iterating over replace_const.expr_map!

Definition at line 462 of file constant_propagator.cpp.

Member Data Documentation

◆ is_bottom

bool constant_propagator_domaint::valuest::is_bottom = true

Definition at line 82 of file constant_propagator.h.

◆ replace_const

address_of_aware_replace_symbolt constant_propagator_domaint::valuest::replace_const

Definition at line 81 of file constant_propagator.h.

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