cprover
value_set_fivrt Class Reference

#include <value_set_fivr.h>

Collaboration diagram for value_set_fivrt:
[legend]

Classes

struct  entryt
 
class  object_map_dt
 
class  objectt
 

Public Types

typedef irep_idt idt
 
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)
 
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) const
 
bool insert_to (object_mapt &dest, unsigned n, const objectt &object) const
 
bool insert_to (object_mapt &dest, const exprt &expr, const objectt &object) 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) const
 
bool insert_from (object_mapt &dest, unsigned n, const objectt &object) const
 
bool insert_from (object_mapt &dest, const exprt &expr, const objectt &object) 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 make_any ()
 
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)
 
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 exprt &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 do_free (const exprt &op, const namespacet &ns)
 
void flatten (const entryt &e, object_mapt &dest) const
 
void flatten_rec (const entryt &, object_mapt &, flatten_seent &, unsigned from_function, unsigned from_index) const
 
bool recursive_find (const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
 

Detailed Description

Definition at line 26 of file value_set_fivr.h.

Member Typedef Documentation

◆ assign_recursion_sett

Definition at line 236 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 223 of file value_set_fivr.h.

◆ expr_sett

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

Definition at line 221 of file value_set_fivr.h.

◆ flatten_seent

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

Definition at line 233 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 234 of file value_set_fivr.h.

◆ idt

Definition at line 50 of file value_set_fivr.h.

◆ object_mapt

◆ recfind_recursion_sett

Definition at line 235 of file value_set_fivr.h.

◆ valuest

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

Definition at line 232 of file value_set_fivr.h.

Constructor & Destructor Documentation

◆ value_set_fivrt()

value_set_fivrt::value_set_fivrt ( )
inline

Definition at line 29 of file value_set_fivr.h.

Member Function Documentation

◆ add_var() [1/2]

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

Definition at line 258 of file value_set_fivr.h.

References get_entry().

Referenced by add_vars(), and do_function_call().

◆ add_var() [2/2]

void value_set_fivrt::add_var ( const entryt e)
inline

◆ add_vars()

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

Definition at line 289 of file value_set_fivr.h.

References add_var().

Referenced by value_set_analysis_fivrt::add_vars().

◆ apply_code()

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

◆ assign()

◆ assign_rec()

◆ clear()

void value_set_fivrt::clear ( void  )
inline

Definition at line 253 of file value_set_fivr.h.

References values.

Referenced by value_set_domain_fivrt::clear(), and value_set_domain_fivrt::initialize().

◆ copy_objects()

◆ dereference_rec()

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

Definition at line 802 of file value_set_fivr.cpp.

References irept::id(), exprt::op0(), exprt::operands(), and exprt::type().

◆ do_end_function()

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

◆ do_free()

◆ 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()

◆ 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 idt id,
const std::string &  suffix 
)
inline

Definition at line 268 of file value_set_fivr.h.

Referenced by add_var(), and assign_rec().

◆ get_entry() [2/2]

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

◆ get_reference_set()

◆ 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 364 of file value_set_fivr.h.

References get_reference_set_sharing_rec().

◆ get_reference_set_sharing_rec()

◆ get_temporary_entry()

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

Definition at line 283 of file value_set_fivr.h.

References id2string(), and temporary_values.

Referenced by assign_rec(), and do_free().

◆ get_value_set() [1/2]

◆ get_value_set() [2/2]

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

Definition at line 474 of file value_set_fivr.cpp.

References get_value_set_rec(), simplify(), and exprt::type().

◆ get_value_set_rec()

◆ handover()

◆ insert_from() [1/5]

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

◆ insert_from() [2/5]

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

◆ insert_from() [3/5]

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

◆ insert_from() [4/5]

◆ insert_from() [5/5]

bool value_set_fivrt::insert_from ( object_mapt dest,
const exprt expr,
const objectt object 
) const
inline

◆ insert_to() [1/5]

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

Definition at line 150 of file value_set_fivr.h.

Referenced by do_free(), insert_to(), make_union(), and make_valid_union().

◆ insert_to() [2/5]

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

◆ insert_to() [3/5]

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

◆ insert_to() [4/5]

◆ insert_to() [5/5]

bool value_set_fivrt::insert_to ( object_mapt dest,
const exprt expr,
const objectt object 
) const
inline

◆ make_any()

void value_set_fivrt::make_any ( )
inline

Definition at line 248 of file value_set_fivr.h.

References values.

◆ 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

Definition at line 381 of file value_set_fivr.cpp.

References forall_valid_objects, insert_to(), and reference_counting< T >::read().

Referenced by assign_rec().

◆ output()

◆ 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 145 of file value_set_fivr.h.

References reference_counting< T >::write().

◆ set_from()

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

◆ set_to()

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

◆ to_expr()

Member Data Documentation

◆ from_function

◆ from_target_index

unsigned value_set_fivrt::from_target_index

◆ function_numbering

hash_numbering< irep_idt, irep_id_hash > value_set_fivrt::function_numbering
static

Definition at line 36 of file value_set_fivr.h.

Referenced by value_set_analysis_fivrt::get_values(), output(), set_from(), and set_to().

◆ object_numbering

◆ temporary_values

valuest value_set_fivrt::temporary_values

Definition at line 303 of file value_set_fivr.h.

Referenced by do_function_call(), get_temporary_entry(), and handover().

◆ to_function

unsigned value_set_fivrt::to_function

◆ to_target_index

unsigned value_set_fivrt::to_target_index

◆ values


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