cprover
value_sett Class Reference

#include <value_set.h>

Collaboration diagram for value_sett:
[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::set< exprtexpr_sett
 
typedef std::set< unsigned int > dynamic_object_id_sett
 
typedef std::unordered_map< idt, entryt, string_hashvaluest
 

Public Member Functions

 value_sett ()
 
exprt to_expr (object_map_dt::const_iterator it) const
 
void set (object_mapt &dest, object_map_dt::const_iterator it) const
 
bool insert (object_mapt &dest, object_map_dt::const_iterator it) const
 
bool insert (object_mapt &dest, const exprt &src) const
 
bool insert (object_mapt &dest, const exprt &src, const mp_integer &offset) const
 
bool insert (object_mapt &dest, unsigned n, const objectt &object) const
 
bool insert (object_mapt &dest, const exprt &expr, const objectt &object) const
 
void get_value_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
 
expr_settget (const idt &identifier, const std::string &suffix)
 
void make_any ()
 
void clear ()
 
entrytget_entry (const entryt &e, const typet &type, const namespacet &)
 
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_sett &new_values)
 
void guard (const exprt &expr, const namespacet &ns)
 
void apply_code (const codet &code, const namespacet &ns)
 
void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
 
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, value_setst::valuest &dest, const namespacet &ns) const
 
bool eval_pointer_offset (exprt &expr, const namespacet &ns) const
 

Static Public Member Functions

static bool field_sensitive (const irep_idt &id, const typet &type, const namespacet &)
 

Public Attributes

unsigned location_number
 
valuest values
 

Static Public Attributes

static object_numberingt object_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, bool is_simplified) 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)
 
exprt make_member (const exprt &src, const irep_idt &component_name, const namespacet &ns)
 

Detailed Description

Definition at line 25 of file value_set.h.

Member Typedef Documentation

◆ dynamic_object_id_sett

typedef std::set<unsigned int> value_sett::dynamic_object_id_sett

Definition at line 121 of file value_set.h.

◆ expr_sett

typedef std::set<exprt> value_sett::expr_sett

Definition at line 119 of file value_set.h.

◆ idt

Definition at line 40 of file value_set.h.

◆ object_mapt

◆ valuest

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

Definition at line 126 of file value_set.h.

Constructor & Destructor Documentation

◆ value_sett()

value_sett::value_sett ( )
inline

Definition at line 28 of file value_set.h.

Member Function Documentation

◆ apply_code()

◆ assign()

◆ assign_rec()

◆ clear()

void value_sett::clear ( void  )
inline

Definition at line 143 of file value_set.h.

References values.

Referenced by value_set_domaint::initialize().

◆ dereference_rec()

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

Definition at line 891 of file value_set.cpp.

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

◆ do_end_function()

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

◆ do_free()

◆ do_function_call()

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

◆ eval_pointer_offset()

bool value_sett::eval_pointer_offset ( exprt expr,
const namespacet ns 
) const

◆ field_sensitive()

bool value_sett::field_sensitive ( const irep_idt id,
const typet type,
const namespacet ns 
)
static

◆ get()

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

◆ get_entry()

value_sett::entryt & value_sett::get_entry ( const entryt e,
const typet type,
const namespacet ns 
)

◆ get_reference_set() [1/2]

void value_sett::get_reference_set ( const exprt expr,
value_setst::valuest dest,
const namespacet ns 
) const

◆ get_reference_set() [2/2]

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

Definition at line 218 of file value_set.h.

References get_reference_set_rec().

◆ get_reference_set_rec()

◆ get_value_set() [1/2]

void value_sett::get_value_set ( const exprt expr,
value_setst::valuest dest,
const namespacet ns 
) const

◆ get_value_set() [2/2]

void value_sett::get_value_set ( const exprt expr,
object_mapt dest,
const namespacet ns,
bool  is_simplified 
) const
protected

◆ get_value_set_rec()

◆ guard()

void value_sett::guard ( const exprt expr,
const namespacet ns 
)

◆ insert() [1/5]

bool value_sett::insert ( object_mapt dest,
object_map_dt::const_iterator  it 
) const
inline

Definition at line 77 of file value_set.h.

Referenced by do_free(), get_reference_set_rec(), get_value_set_rec(), insert(), and make_union().

◆ insert() [2/5]

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

Definition at line 82 of file value_set.h.

References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.

◆ insert() [3/5]

bool value_sett::insert ( object_mapt dest,
const exprt src,
const mp_integer offset 
) const
inline

Definition at line 87 of file value_set.h.

References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.

◆ insert() [4/5]

bool value_sett::insert ( object_mapt dest,
unsigned  n,
const objectt object 
) const

◆ insert() [5/5]

bool value_sett::insert ( object_mapt dest,
const exprt expr,
const objectt object 
) const
inline

Definition at line 97 of file value_set.h.

References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.

◆ make_any()

void value_sett::make_any ( )
inline

Definition at line 138 of file value_set.h.

References values.

◆ make_member()

◆ make_union() [1/3]

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

◆ make_union() [2/3]

bool value_sett::make_union ( const valuest new_values)

Definition at line 207 of file value_set.cpp.

References make_union(), value_sett::entryt::object_map, and values.

◆ make_union() [3/3]

bool value_sett::make_union ( const value_sett new_values)
inline

Definition at line 165 of file value_set.h.

References make_union(), and values.

◆ output()

◆ set()

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

Definition at line 72 of file value_set.h.

References reference_counting< T >::write().

◆ to_expr()

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

Member Data Documentation

◆ location_number

unsigned value_sett::location_number

Definition at line 37 of file value_set.h.

Referenced by get_value_set_rec(), and value_set_domaint::initialize().

◆ object_numbering

object_numberingt value_sett::object_numbering
static

◆ values

valuest value_sett::values

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