cprover
|
#include <var_map.h>
Public Types | |
enum | { SHARED, THREAD_LOCAL, PROCEDURE_LOCAL } |
Public Member Functions | |
bool | is_shared () const |
var_infot () | |
irep_idt | ssa_identifier () const |
symbol_exprt | ssa_symbol () const |
void | increment_ssa_counter () |
void | output (std::ostream &out) const |
Public Attributes | |
enum var_mapt::var_infot:: { ... } | kind |
unsigned | number |
irep_idt | full_identifier |
irep_idt | symbol |
irep_idt | suffix |
typet | type |
unsigned | ssa_counter |
anonymous enum |
|
inline |
Definition at line 69 of file var_map.h.
References ssa_counter.
Referenced by path_symext::assign_rec().
|
inline |
Definition at line 39 of file var_map.h.
Referenced by path_symex_statet::get_var_state(), and var_mapt::init().
void var_mapt::var_infot::output | ( | std::ostream & | out | ) | const |
Definition at line 47 of file var_map.cpp.
References full_identifier, kind, number, irept::pretty(), PROCEDURE_LOCAL, SHARED, suffix, symbol, THREAD_LOCAL, and type.
irep_idt var_mapt::var_infot::ssa_identifier | ( | ) | const |
|
inline |
Definition at line 61 of file var_map.h.
References full_identifier, irept::set(), ssa_identifier(), and type.
Referenced by path_symext::assign_rec(), and path_symex_statet::read_symbol_member_index().
irep_idt var_mapt::var_infot::full_identifier |
Definition at line 48 of file var_map.h.
Referenced by path_symext::assign_rec(), var_mapt::init(), output(), path_symex_statet::read_symbol_member_index(), ssa_symbol(), and path_symext::symex_va_arg_next().
enum { ... } var_mapt::var_infot::kind |
Referenced by var_mapt::init(), is_shared(), and output().
unsigned var_mapt::var_infot::number |
Definition at line 45 of file var_map.h.
Referenced by path_symex_statet::get_var_state(), var_mapt::init(), and output().
unsigned var_mapt::var_infot::ssa_counter |
Definition at line 53 of file var_map.h.
Referenced by increment_ssa_counter().
irep_idt var_mapt::var_infot::suffix |
irep_idt var_mapt::var_infot::symbol |
Definition at line 48 of file var_map.h.
Referenced by var_mapt::init(), and output().
typet var_mapt::var_infot::type |
Definition at line 51 of file var_map.h.
Referenced by output(), and ssa_symbol().