cprover
value_set_fit Class Reference

#include <value_set_fi.h>

+ Collaboration diagram for value_set_fit:

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_fit ()
 
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 (const object_map_dt::value_type &it) const
 
void set (object_mapt &dest, const object_map_dt::value_type &it) const
 
bool insert (object_mapt &dest, const object_map_dt::value_type &it) const
 
bool insert (object_mapt &dest, const exprt &src) const
 
bool insert (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
 
bool insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
 
bool insert (object_mapt &dest, const exprt &expr, const offsett &offset) const
 
void get_value_set (const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
 
expr_settget (const idt &identifier, const std::string &suffix)
 
void clear ()
 
void add_var (const idt &id, const std::string &suffix)
 
void add_var (const entryt &e)
 
entrytget_entry (const idt &id, const std::string &suffix)
 
entrytget_entry (const entryt &e)
 
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_union (const valuest &new_values)
 
bool make_union (const value_set_fit &new_values)
 
void apply_code (const exprt &code, const namespacet &ns)
 
void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns)
 
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
 
bool changed
 

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)
 
void flatten (const entryt &e, object_mapt &dest) const
 
void flatten_rec (const entryt &, object_mapt &, flatten_seent &) const
 

Detailed Description

Definition at line 27 of file value_set_fi.h.

Member Typedef Documentation

◆ assign_recursion_sett

Definition at line 203 of file value_set_fi.h.

◆ dynamic_object_id_sett

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

Definition at line 190 of file value_set_fi.h.

◆ expr_sett

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

Definition at line 188 of file value_set_fi.h.

◆ flatten_seent

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

Definition at line 200 of file value_set_fi.h.

◆ gvs_recursion_sett

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

Definition at line 201 of file value_set_fi.h.

◆ idt

Definition at line 54 of file value_set_fi.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 58 of file value_set_fi.h.

◆ recfind_recursion_sett

Definition at line 202 of file value_set_fi.h.

◆ valuest

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

Definition at line 199 of file value_set_fi.h.

Constructor & Destructor Documentation

◆ value_set_fit()

value_set_fit::value_set_fit ( )
inline

Definition at line 30 of file value_set_fi.h.

Member Function Documentation

◆ add_var() [1/2]

void value_set_fit::add_var ( const idt id,
const std::string &  suffix 
)
inline

Definition at line 220 of file value_set_fi.h.

◆ add_var() [2/2]

void value_set_fit::add_var ( const entryt e)
inline

Definition at line 225 of file value_set_fi.h.

◆ add_vars()

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

Definition at line 245 of file value_set_fi.h.

◆ apply_code()

void value_set_fit::apply_code ( const exprt code,
const namespacet ns 
)

Definition at line 1332 of file value_set_fi.cpp.

◆ assign()

void value_set_fit::assign ( const exprt lhs,
const exprt rhs,
const namespacet ns 
)

Definition at line 957 of file value_set_fi.cpp.

◆ assign_rec()

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

Definition at line 1118 of file value_set_fi.cpp.

◆ clear()

void value_set_fit::clear ( void  )
inline

Definition at line 215 of file value_set_fi.h.

◆ dereference_rec()

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

Definition at line 687 of file value_set_fi.cpp.

◆ do_end_function()

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

Definition at line 1319 of file value_set_fi.cpp.

◆ do_function_call()

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

Definition at line 1270 of file value_set_fi.cpp.

◆ flatten()

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

Definition at line 139 of file value_set_fi.cpp.

◆ flatten_rec()

void value_set_fit::flatten_rec ( const entryt e,
object_mapt dest,
flatten_seent seen 
) const
protected

Definition at line 155 of file value_set_fi.cpp.

◆ get()

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

◆ get_entry() [1/2]

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

Definition at line 230 of file value_set_fi.h.

◆ get_entry() [2/2]

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

Definition at line 235 of file value_set_fi.h.

◆ get_reference_set()

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

Definition at line 705 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [1/2]

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

Definition at line 753 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [2/2]

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

Definition at line 318 of file value_set_fi.h.

◆ get_reference_set_sharing_rec()

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

Definition at line 765 of file value_set_fi.cpp.

◆ get_value_set() [1/2]

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

Definition at line 296 of file value_set_fi.cpp.

◆ get_value_set() [2/2]

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

Definition at line 357 of file value_set_fi.cpp.

◆ get_value_set_rec()

void value_set_fit::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

Definition at line 369 of file value_set_fi.cpp.

◆ insert() [1/5]

bool value_set_fit::insert ( object_mapt dest,
const object_map_dt::value_type it 
) const
inline

Definition at line 113 of file value_set_fi.h.

◆ insert() [2/5]

bool value_set_fit::insert ( object_mapt dest,
const exprt src 
) const
inline

Definition at line 118 of file value_set_fi.h.

◆ insert() [3/5]

bool value_set_fit::insert ( object_mapt dest,
const exprt src,
const mp_integer offset_value 
) const
inline

Definition at line 123 of file value_set_fi.h.

◆ insert() [4/5]

bool value_set_fit::insert ( object_mapt dest,
object_numberingt::number_type  n,
const offsett offset 
) const
inline

Definition at line 131 of file value_set_fi.h.

◆ insert() [5/5]

bool value_set_fit::insert ( object_mapt dest,
const exprt expr,
const offsett offset 
) const
inline

Definition at line 166 of file value_set_fi.h.

◆ make_union() [1/3]

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

Definition at line 283 of file value_set_fi.cpp.

◆ make_union() [2/3]

bool value_set_fit::make_union ( const valuest new_values)

Definition at line 244 of file value_set_fi.cpp.

◆ make_union() [3/3]

bool value_set_fit::make_union ( const value_set_fit new_values)
inline

Definition at line 269 of file value_set_fi.h.

◆ offset_is_zero()

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

Definition at line 59 of file value_set_fi.h.

◆ output()

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

Definition at line 45 of file value_set_fi.cpp.

◆ set()

void value_set_fit::set ( object_mapt dest,
const object_map_dt::value_type it 
) const
inline

Definition at line 108 of file value_set_fi.h.

◆ set_from()

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

Definition at line 42 of file value_set_fi.h.

◆ set_to()

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

Definition at line 48 of file value_set_fi.h.

◆ to_expr()

exprt value_set_fit::to_expr ( const object_map_dt::value_type it) const

Definition at line 224 of file value_set_fi.cpp.

Member Data Documentation

◆ changed

bool value_set_fit::changed

Definition at line 260 of file value_set_fi.h.

◆ from_function

unsigned value_set_fit::from_function

Definition at line 37 of file value_set_fi.h.

◆ from_target_index

unsigned value_set_fit::from_target_index

Definition at line 38 of file value_set_fi.h.

◆ function_numbering

hash_numbering< irep_idt, irep_id_hash > value_set_fit::function_numbering
static

Definition at line 40 of file value_set_fi.h.

◆ object_numbering

object_numberingt value_set_fit::object_numbering
static

Definition at line 39 of file value_set_fi.h.

◆ to_function

unsigned value_set_fit::to_function

Definition at line 37 of file value_set_fi.h.

◆ to_target_index

unsigned value_set_fit::to_target_index

Definition at line 38 of file value_set_fi.h.

◆ values

valuest value_set_fit::values

Definition at line 258 of file value_set_fi.h.


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