cprover
value_set_fit Class Reference

#include <value_set_fi.h>

Collaboration diagram for value_set_fit:
[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_fit ()
 
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 (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, std::list< exprt > &dest, 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)
 
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 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 &) const
 

Detailed Description

Definition at line 26 of file value_set_fi.h.

Member Typedef Documentation

§ assign_recursion_sett

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

§ expr_sett

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

Definition at line 159 of file value_set_fi.h.

§ flatten_seent

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

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

§ idt

Definition at line 50 of file value_set_fi.h.

§ object_mapt

§ recfind_recursion_sett

Definition at line 173 of file value_set_fi.h.

§ valuest

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

Definition at line 170 of file value_set_fi.h.

Constructor & Destructor Documentation

§ value_set_fit()

value_set_fit::value_set_fit ( )
inline

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

References get_entry().

Referenced by add_vars(), and do_function_call().

§ add_var() [2/2]

void value_set_fit::add_var ( const entryt e)
inline

§ add_vars()

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

Definition at line 221 of file value_set_fi.h.

References add_var(), and output().

Referenced by value_set_analysis_fit::add_vars().

§ apply_code()

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

§ assign()

§ assign_rec()

§ clear()

void value_set_fit::clear ( void  )
inline

Definition at line 191 of file value_set_fi.h.

References values.

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

§ dereference_rec()

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

Definition at line 688 of file value_set_fi.cpp.

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

Referenced by get_reference_set_sharing().

§ do_end_function()

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

Definition at line 1404 of file value_set_fi.cpp.

References assign(), from_function, irept::is_nil(), and exprt::type().

Referenced by make_union(), and value_set_domain_fit::transform().

§ do_free()

§ do_function_call()

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

§ flatten()

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

§ flatten_rec()

§ 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 206 of file value_set_fi.h.

Referenced by add_var(), and assign_rec().

§ get_entry() [2/2]

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

§ get_reference_set()

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

§ 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

§ 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

§ get_reference_set_sharing_rec()

§ get_value_set() [1/2]

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

§ 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 359 of file value_set_fi.cpp.

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

§ get_value_set_rec()

§ insert() [1/5]

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

§ insert() [2/5]

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

§ insert() [3/5]

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

§ insert() [4/5]

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

§ insert() [5/5]

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

Definition at line 137 of file value_set_fi.h.

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

§ make_any()

void value_set_fit::make_any ( )
inline

Definition at line 186 of file value_set_fi.h.

References values.

§ make_union() [1/3]

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

§ make_union() [2/3]

bool value_set_fit::make_union ( const valuest new_values)

§ make_union() [3/3]

bool value_set_fit::make_union ( const value_set_fit new_values)
inline

§ output()

§ set()

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

Definition at line 82 of file value_set_fi.h.

References reference_counting< T >::write().

§ set_from()

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

Definition at line 38 of file value_set_fi.h.

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

Referenced by value_set_domain_fit::transform().

§ set_to()

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

Definition at line 44 of file value_set_fi.h.

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

Referenced by value_set_domain_fit::transform().

§ to_expr()

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

Member Data Documentation

§ changed

bool value_set_fit::changed

Definition at line 236 of file value_set_fi.h.

Referenced by assign_rec(), do_free(), make_union(), and value_set_domain_fit::transform().

§ from_function

unsigned value_set_fit::from_function

§ from_target_index

unsigned value_set_fit::from_target_index

Definition at line 34 of file value_set_fi.h.

Referenced by get_value_set_rec(), and value_set_analysis_fit::get_values().

§ function_numbering

hash_numbering< irep_idt, irep_id_hash > value_set_fit::function_numbering
static

Definition at line 36 of file value_set_fi.h.

Referenced by value_set_analysis_fit::get_values().

§ object_numbering

§ to_function

unsigned value_set_fit::to_function

Definition at line 33 of file value_set_fi.h.

Referenced by value_set_analysis_fit::get_values().

§ to_target_index

unsigned value_set_fit::to_target_index

Definition at line 34 of file value_set_fi.h.

Referenced by value_set_analysis_fit::get_values().

§ values


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