cprover
value_set_fivrnst Class Reference

#include <value_set_fivrns.h>

Collaboration diagram for value_set_fivrnst:
[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
 

Public Member Functions

 value_set_fivrnst ()
 
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
 
void output_entry (const entryt &e, 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_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
 
void get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 
void get_reference_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 
void get_reference_set_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, bool add_to_sets)
 
void do_free (const exprt &op, const namespacet &ns)
 

Detailed Description

Definition at line 27 of file value_set_fivrns.h.

Member Typedef Documentation

◆ dynamic_object_id_sett

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

Definition at line 223 of file value_set_fivrns.h.

◆ expr_sett

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

Definition at line 221 of file value_set_fivrns.h.

◆ idt

Definition at line 51 of file value_set_fivrns.h.

◆ object_mapt

◆ valuest

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

Definition at line 228 of file value_set_fivrns.h.

Constructor & Destructor Documentation

◆ value_set_fivrnst()

value_set_fivrnst::value_set_fivrnst ( )
inline

Definition at line 30 of file value_set_fivrns.h.

Member Function Documentation

◆ add_var() [1/2]

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

Definition at line 250 of file value_set_fivrns.h.

References get_entry().

Referenced by add_vars(), apply_code(), do_end_function(), and do_function_call().

◆ add_var() [2/2]

void value_set_fivrnst::add_var ( const entryt e)
inline

◆ add_vars()

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

Definition at line 281 of file value_set_fivrns.h.

References add_var().

Referenced by value_set_analysis_fivrnst::add_vars().

◆ apply_code()

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

◆ assign()

◆ assign_rec()

◆ clear()

void value_set_fivrnst::clear ( void  )
inline

Definition at line 245 of file value_set_fivrns.h.

References values.

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

◆ copy_objects()

◆ dereference_rec()

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

Definition at line 588 of file value_set_fivrns.cpp.

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

◆ do_end_function()

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

◆ do_free()

◆ do_function_call()

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

◆ get()

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

◆ get_entry() [1/2]

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

Definition at line 260 of file value_set_fivrns.h.

Referenced by add_var(), and assign_rec().

◆ get_entry() [2/2]

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

◆ get_reference_set() [1/2]

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

◆ get_reference_set() [2/2]

void value_set_fivrnst::get_reference_set ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
inlineprotected

Definition at line 355 of file value_set_fivrns.h.

References get_reference_set_rec().

◆ get_reference_set_rec()

◆ get_temporary_entry()

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

Definition at line 275 of file value_set_fivrns.h.

References id2string(), and temporary_values.

Referenced by assign_rec(), and do_free().

◆ get_value_set() [1/2]

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

◆ get_value_set() [2/2]

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

Definition at line 284 of file value_set_fivrns.cpp.

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

◆ get_value_set_rec()

◆ handover()

◆ insert_from() [1/5]

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

Definition at line 178 of file value_set_fivrns.h.

Referenced by get_reference_set_rec(), get_value_set_rec(), and insert_from().

◆ insert_from() [2/5]

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

◆ insert_from() [3/5]

bool value_set_fivrnst::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_fivrnst::insert_from ( object_mapt dest,
const exprt expr,
const objectt object 
) const
inline

◆ insert_to() [1/5]

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

Definition at line 150 of file value_set_fivrns.h.

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

◆ insert_to() [2/5]

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

◆ insert_to() [3/5]

bool value_set_fivrnst::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_fivrnst::insert_to ( object_mapt dest,
const exprt expr,
const objectt object 
) const
inline

◆ make_any()

void value_set_fivrnst::make_any ( )
inline

Definition at line 240 of file value_set_fivrns.h.

References values.

◆ make_union()

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

◆ make_valid_union()

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

Definition at line 237 of file value_set_fivrns.cpp.

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

Referenced by assign_rec().

◆ output()

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

Definition at line 57 of file value_set_fivrns.cpp.

References output_entry(), and values.

Referenced by value_set_domain_fivrnst::output().

◆ output_entry()

◆ set()

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

Definition at line 145 of file value_set_fivrns.h.

References reference_counting< T >::write().

◆ set_from()

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

◆ set_to()

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

◆ to_expr()

Member Data Documentation

◆ from_function

◆ from_target_index

unsigned value_set_fivrnst::from_target_index

◆ function_numbering

hash_numbering< irep_idt, irep_id_hash > value_set_fivrnst::function_numbering
static

◆ object_numbering

object_numberingt value_set_fivrnst::object_numbering
static

◆ temporary_values

valuest value_set_fivrnst::temporary_values

Definition at line 300 of file value_set_fivrns.h.

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

◆ to_function

unsigned value_set_fivrnst::to_function

◆ to_target_index

unsigned value_set_fivrnst::to_target_index

◆ values

valuest value_set_fivrnst::values

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