cprover
value_set_fivrt Class Reference

#include <value_set_fivr.h>

+ Collaboration diagram for value_set_fivrt:

Classes

struct  entryt
 
class  object_map_dt
 

Public Types

typedef irep_idt idt
 
typedef optionalt< mp_integeroffsett
 Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset. More...
 
typedef reference_counting< object_map_dtobject_mapt
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 
typedef std::unordered_set< unsigned int > dynamic_object_id_sett
 
typedef std::unordered_map< idt, entryt, string_hashvaluest
 
typedef std::unordered_set< idt, string_hashflatten_seent
 
typedef std::unordered_set< idt, string_hashgvs_recursion_sett
 
typedef std::unordered_set< idt, string_hashrecfind_recursion_sett
 
typedef std::unordered_set< idt, string_hashassign_recursion_sett
 

Public Member Functions

 value_set_fivrt ()
 
void set_from (const irep_idt &function, unsigned inx)
 
void set_to (const irep_idt &function, unsigned inx)
 
bool offset_is_zero (const offsett &offset) const
 
exprt to_expr (object_map_dt::const_iterator it) const
 
void set (object_mapt &dest, object_map_dt::const_iterator it) const
 
bool insert_to (object_mapt &dest, object_map_dt::const_iterator it) const
 
bool insert_to (object_mapt &dest, const exprt &src) const
 
bool insert_to (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
 
bool insert_to (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
 
bool insert_to (object_mapt &dest, const exprt &expr, const offsett &offset) const
 
bool insert_from (object_mapt &dest, object_map_dt::const_iterator it) const
 
bool insert_from (object_mapt &dest, const exprt &src) const
 
bool insert_from (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
 
bool insert_from (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
 
bool insert_from (object_mapt &dest, const exprt &expr, const offsett &offset) const
 
void get_value_set (const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
 
expr_settget (const idt &identifier, const std::string &suffix)
 
void clear ()
 
void add_var (const idt &id)
 
void add_var (const entryt &e)
 
entrytget_entry (const idt &id, const std::string &suffix)
 
entrytget_entry (const entryt &e)
 
entrytget_temporary_entry (const idt &id, const std::string &suffix)
 
void add_vars (const std::list< entryt > &vars)
 
void output (const namespacet &ns, std::ostream &out) const
 
bool make_union (object_mapt &dest, const object_mapt &src) const
 
bool make_valid_union (object_mapt &dest, const object_mapt &src) const
 
void copy_objects (object_mapt &dest, const object_mapt &src) const
 
void apply_code (const codet &code, const namespacet &ns)
 
bool handover ()
 
void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
 
void do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
 
void do_end_function (const exprt &lhs, const namespacet &ns)
 
void get_reference_set (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
 

Public Attributes

unsigned to_function
 
unsigned from_function
 
unsigned to_target_index
 
unsigned from_target_index
 
valuest values
 
valuest temporary_values
 

Static Public Attributes

static object_numberingt object_numbering
 
static hash_numbering< irep_idt, irep_id_hashfunction_numbering
 

Protected Member Functions

void get_reference_set_sharing (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
 
void get_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
 
void get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 
void get_reference_set_sharing (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 
void get_reference_set_sharing_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 
void dereference_rec (const exprt &src, exprt &dest) const
 
void assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets)
 
void flatten (const entryt &e, object_mapt &dest) const
 
void flatten_rec (const entryt &, object_mapt &, flatten_seent &, unsigned from_function) const
 
bool recursive_find (const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
 

Detailed Description

Definition at line 29 of file value_set_fivr.h.

Member Typedef Documentation

◆ assign_recursion_sett

Definition at line 235 of file value_set_fivr.h.

◆ dynamic_object_id_sett

typedef std::unordered_set<unsigned int> value_set_fivrt::dynamic_object_id_sett

Definition at line 222 of file value_set_fivr.h.

◆ expr_sett

typedef std::unordered_set<exprt, irep_hash> value_set_fivrt::expr_sett

Definition at line 220 of file value_set_fivr.h.

◆ flatten_seent

typedef std::unordered_set<idt, string_hash> value_set_fivrt::flatten_seent

Definition at line 232 of file value_set_fivr.h.

◆ gvs_recursion_sett

typedef std::unordered_set<idt, string_hash> value_set_fivrt::gvs_recursion_sett

Definition at line 233 of file value_set_fivr.h.

◆ idt

Definition at line 53 of file value_set_fivr.h.

◆ object_mapt

◆ offsett

Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.

Definition at line 57 of file value_set_fivr.h.

◆ recfind_recursion_sett

Definition at line 234 of file value_set_fivr.h.

◆ valuest

typedef std::unordered_map<idt, entryt, string_hash> value_set_fivrt::valuest

Definition at line 231 of file value_set_fivr.h.

Constructor & Destructor Documentation

◆ value_set_fivrt()

value_set_fivrt::value_set_fivrt ( )
inline

Definition at line 32 of file value_set_fivr.h.

Member Function Documentation

◆ add_var() [1/2]

void value_set_fivrt::add_var ( const entryt e)
inline

Definition at line 257 of file value_set_fivr.h.

◆ add_var() [2/2]

void value_set_fivrt::add_var ( const idt id)
inline

Definition at line 252 of file value_set_fivr.h.

◆ add_vars()

void value_set_fivrt::add_vars ( const std::list< entryt > &  vars)
inline

Definition at line 283 of file value_set_fivr.h.

◆ apply_code()

void value_set_fivrt::apply_code ( const codet code,
const namespacet ns 
)

◆ assign()

void value_set_fivrt::assign ( const exprt lhs,
const exprt rhs,
const namespacet ns,
bool  add_to_sets = false 
)

◆ assign_rec()

void value_set_fivrt::assign_rec ( const exprt lhs,
const object_mapt values_rhs,
const std::string &  suffix,
const namespacet ns,
assign_recursion_sett recursion_set,
bool  add_to_sets 
)
protected

◆ clear()

void value_set_fivrt::clear ( void  )
inline

Definition at line 247 of file value_set_fivr.h.

◆ copy_objects()

void value_set_fivrt::copy_objects ( object_mapt dest,
const object_mapt src 
) const

◆ dereference_rec()

void value_set_fivrt::dereference_rec ( const exprt src,
exprt dest 
) const
protected

◆ do_end_function()

void value_set_fivrt::do_end_function ( const exprt lhs,
const namespacet ns 
)

◆ do_function_call()

void value_set_fivrt::do_function_call ( const irep_idt function,
const exprt::operandst arguments,
const namespacet ns 
)

◆ flatten()

void value_set_fivrt::flatten ( const entryt e,
object_mapt dest 
) const
protected

◆ flatten_rec()

void value_set_fivrt::flatten_rec ( const entryt ,
object_mapt ,
flatten_seent ,
unsigned  from_function 
) const
protected

◆ get()

expr_sett& value_set_fivrt::get ( const idt identifier,
const std::string &  suffix 
)

◆ get_entry() [1/2]

entryt& value_set_fivrt::get_entry ( const entryt e)
inline

Definition at line 267 of file value_set_fivr.h.

◆ get_entry() [2/2]

entryt& value_set_fivrt::get_entry ( const idt id,
const std::string &  suffix 
)
inline

Definition at line 262 of file value_set_fivr.h.

◆ get_reference_set()

void value_set_fivrt::get_reference_set ( const exprt expr,
expr_sett expr_set,
const namespacet ns 
) const

◆ get_reference_set_sharing() [1/2]

void value_set_fivrt::get_reference_set_sharing ( const exprt expr,
expr_sett expr_set,
const namespacet ns 
) const
protected

◆ get_reference_set_sharing() [2/2]

void value_set_fivrt::get_reference_set_sharing ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
inlineprotected

Definition at line 356 of file value_set_fivr.h.

◆ get_reference_set_sharing_rec()

void value_set_fivrt::get_reference_set_sharing_rec ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
protected

◆ get_temporary_entry()

entryt& value_set_fivrt::get_temporary_entry ( const idt id,
const std::string &  suffix 
)
inline

Definition at line 277 of file value_set_fivr.h.

◆ get_value_set() [1/2]

void value_set_fivrt::get_value_set ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
protected

◆ get_value_set() [2/2]

void value_set_fivrt::get_value_set ( const exprt expr,
std::list< exprt > &  expr_set,
const namespacet ns 
) const

◆ get_value_set_rec()

void value_set_fivrt::get_value_set_rec ( const exprt expr,
object_mapt dest,
const std::string &  suffix,
const typet original_type,
const namespacet ns,
gvs_recursion_sett recursion_set 
) const
protected

◆ handover()

bool value_set_fivrt::handover ( )

◆ insert_from() [1/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
const exprt expr,
const offsett offset 
) const
inline

Definition at line 200 of file value_set_fivr.h.

◆ insert_from() [2/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
const exprt src 
) const
inline

Definition at line 180 of file value_set_fivr.h.

◆ insert_from() [3/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
const exprt src,
const mp_integer offset_value 
) const
inline

Definition at line 185 of file value_set_fivr.h.

◆ insert_from() [4/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
object_map_dt::const_iterator  it 
) const
inline

Definition at line 175 of file value_set_fivr.h.

◆ insert_from() [5/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
object_numberingt::number_type  n,
const offsett offset 
) const

◆ insert_to() [1/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
const exprt expr,
const offsett offset 
) const
inline

Definition at line 170 of file value_set_fivr.h.

◆ insert_to() [2/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
const exprt src 
) const
inline

Definition at line 151 of file value_set_fivr.h.

◆ insert_to() [3/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
const exprt src,
const mp_integer offset_value 
) const
inline

Definition at line 156 of file value_set_fivr.h.

◆ insert_to() [4/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
object_map_dt::const_iterator  it 
) const
inline

Definition at line 146 of file value_set_fivr.h.

◆ insert_to() [5/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
object_numberingt::number_type  n,
const offsett offset 
) const

◆ make_union()

bool value_set_fivrt::make_union ( object_mapt dest,
const object_mapt src 
) const

◆ make_valid_union()

bool value_set_fivrt::make_valid_union ( object_mapt dest,
const object_mapt src 
) const

◆ offset_is_zero()

bool value_set_fivrt::offset_is_zero ( const offsett offset) const
inline

Definition at line 58 of file value_set_fivr.h.

◆ output()

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

◆ recursive_find()

bool value_set_fivrt::recursive_find ( const irep_idt ident,
const object_mapt rhs,
recfind_recursion_sett recursion_set 
) const
protected

◆ set()

void value_set_fivrt::set ( object_mapt dest,
object_map_dt::const_iterator  it 
) const
inline

Definition at line 141 of file value_set_fivr.h.

◆ set_from()

void value_set_fivrt::set_from ( const irep_idt function,
unsigned  inx 
)
inline

Definition at line 41 of file value_set_fivr.h.

◆ set_to()

void value_set_fivrt::set_to ( const irep_idt function,
unsigned  inx 
)
inline

Definition at line 47 of file value_set_fivr.h.

◆ to_expr()

exprt value_set_fivrt::to_expr ( object_map_dt::const_iterator  it) const

Member Data Documentation

◆ from_function

unsigned value_set_fivrt::from_function

Definition at line 36 of file value_set_fivr.h.

◆ from_target_index

unsigned value_set_fivrt::from_target_index

Definition at line 37 of file value_set_fivr.h.

◆ function_numbering

hash_numbering<irep_idt, irep_id_hash> value_set_fivrt::function_numbering
static

Definition at line 39 of file value_set_fivr.h.

◆ object_numbering

object_numberingt value_set_fivrt::object_numbering
static

Definition at line 38 of file value_set_fivr.h.

◆ temporary_values

valuest value_set_fivrt::temporary_values

Definition at line 297 of file value_set_fivr.h.

◆ to_function

unsigned value_set_fivrt::to_function

Definition at line 36 of file value_set_fivr.h.

◆ to_target_index

unsigned value_set_fivrt::to_target_index

Definition at line 37 of file value_set_fivr.h.

◆ values

valuest value_set_fivrt::values

Definition at line 296 of file value_set_fivr.h.


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