CBMC
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Public Attributes | Static Public Attributes | Protected Member Functions | List of all members
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 std::optional< mp_integeroffsett
  Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.
 
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 
typedef std::unordered_set< unsigned intdynamic_object_id_sett
 
typedef std::map< idt, entrytvaluest
 
typedef std::set< idtflatten_seent
 
typedef std::unordered_set< idtgvs_recursion_sett
 
typedef std::unordered_set< idtrecfind_recursion_sett
 
typedef std::unordered_set< idtassign_recursion_sett
 

Public Member Functions

 
 
 
 
 
 
 
 
 
 
bool  insert (object_mapt &dest, const exprt &expr, const offsett &offset) const
 
std::vector< exprtget_value_set (const exprt &expr, const namespacet &ns) const
 
expr_settget (const idt &identifier, const std::string &suffix)
 
void  clear ()
 
 
 
entrytget_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
 
 
 
 
 
 
 
 
 

Public Attributes

 
 
 
 
 
 

Static Public Attributes

 
 

Protected Member Functions

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

Detailed Description

Definition at line 29 of file value_set_fi.h.

Member Typedef Documentation

◆  assign_recursion_sett

Definition at line 198 of file value_set_fi.h.

◆  dynamic_object_id_sett

Definition at line 192 of file value_set_fi.h.

◆  expr_sett

Definition at line 190 of file value_set_fi.h.

◆  flatten_seent

Definition at line 195 of file value_set_fi.h.

◆  gvs_recursion_sett

Definition at line 196 of file value_set_fi.h.

◆  idt

Definition at line 56 of file value_set_fi.h.

◆  object_mapt

Definition at line 108 of file value_set_fi.h.

◆  offsett

Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.

Definition at line 60 of file value_set_fi.h.

◆  recfind_recursion_sett

Definition at line 197 of file value_set_fi.h.

◆  valuest

Definition at line 194 of file value_set_fi.h.

Constructor & Destructor Documentation

◆  value_set_fit()

value_set_fit::value_set_fit ( )
inline

Definition at line 32 of file value_set_fi.h.

Member Function Documentation

◆  add_var() [1/2]

void value_set_fit::add_var ( const entryte )
inline

Definition at line 217 of file value_set_fi.h.

◆  add_var() [2/2]

void value_set_fit::add_var ( const idtid )
inline

Definition at line 212 of file value_set_fi.h.

◆  add_vars()

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

Definition at line 237 of file value_set_fi.h.

◆  apply_code()

void value_set_fit::apply_code ( const codetcode,
const namespacetns 
)

Definition at line 1383 of file value_set_fi.cpp.

◆  assign()

void value_set_fit::assign ( const exprtlhs,
const exprtrhs,
const namespacetns 
)

Definition at line 997 of file value_set_fi.cpp.

◆  assign_rec()

void value_set_fit::assign_rec ( const exprtlhs,
const object_maptvalues_rhs,
const std::string &  suffix,
const namespacetns,
assign_recursion_settrecursion_set 
)
protected

Definition at line 1163 of file value_set_fi.cpp.

◆  clear()

void value_set_fit::clear ( )
inline

Definition at line 207 of file value_set_fi.h.

◆  dereference_rec()

void value_set_fit::dereference_rec ( const exprtsrc,
exprtdest 
) const
protected

Definition at line 716 of file value_set_fi.cpp.

◆  do_end_function()

void value_set_fit::do_end_function ( const exprtlhs,
const namespacetns 
)

Definition at line 1370 of file value_set_fi.cpp.

◆  do_function_call()

void value_set_fit::do_function_call ( const irep_idtfunction,
const exprt::operandstarguments,
const namespacetns 
)

Definition at line 1321 of file value_set_fi.cpp.

◆  flatten()

void value_set_fit::flatten ( const entryte,
object_maptdest 
) const
protected

Definition at line 133 of file value_set_fi.cpp.

◆  flatten_rec()

void value_set_fit::flatten_rec ( const entryte,
object_maptdest,
flatten_seentseen 
) const
protected

Definition at line 149 of file value_set_fi.cpp.

◆  get()

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

◆  get_entry() [1/2]

entryt & value_set_fit::get_entry ( const entryte )
inline

Definition at line 227 of file value_set_fi.h.

◆  get_entry() [2/2]

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

Definition at line 222 of file value_set_fi.h.

◆  get_reference_set()

void value_set_fit::get_reference_set ( const exprtexpr,
expr_settexpr_set,
const namespacetns 
) const

Definition at line 731 of file value_set_fi.cpp.

◆  get_reference_set_sharing() [1/2]

void value_set_fit::get_reference_set_sharing ( const exprtexpr,
expr_settexpr_set,
const namespacetns 
) const
protected

Definition at line 779 of file value_set_fi.cpp.

◆  get_reference_set_sharing() [2/2]

void value_set_fit::get_reference_set_sharing ( const exprtexpr,
object_maptdest,
const namespacetns 
) const
inlineprotected

Definition at line 308 of file value_set_fi.h.

◆  get_reference_set_sharing_rec()

void value_set_fit::get_reference_set_sharing_rec ( const exprtexpr,
object_maptdest,
const namespacetns 
) const
protected

Definition at line 791 of file value_set_fi.cpp.

◆  get_value_set() [1/2]

std::vector< exprt > value_set_fit::get_value_set ( const exprtexpr,
const namespacetns 
) const

Definition at line 291 of file value_set_fi.cpp.

◆  get_value_set() [2/2]

void value_set_fit::get_value_set ( const exprtexpr,
object_maptdest,
const namespacetns 
) const
protected

Definition at line 352 of file value_set_fi.cpp.

◆  get_value_set_rec()

void value_set_fit::get_value_set_rec ( const exprtexpr,
object_maptdest,
boolincludes_nondet_pointer,
const std::string &  suffix,
const typetoriginal_type,
const namespacetns,
gvs_recursion_settrecursion_set 
) const
protected

Definition at line 366 of file value_set_fi.cpp.

◆  insert() [1/5]

bool value_set_fit::insert ( object_maptdest,
const exprtexpr,
const offsettoffset 
) const
inline

Definition at line 168 of file value_set_fi.h.

◆  insert() [2/5]

bool value_set_fit::insert ( object_maptdest,
const exprtsrc 
) const
inline

Definition at line 120 of file value_set_fi.h.

◆  insert() [3/5]

bool value_set_fit::insert ( object_maptdest,
const exprtsrc,
const mp_integeroffset_value 
) const
inline

Definition at line 125 of file value_set_fi.h.

◆  insert() [4/5]

bool value_set_fit::insert ( object_maptdest,
) const
inline

Definition at line 115 of file value_set_fi.h.

◆  insert() [5/5]

bool value_set_fit::insert ( object_maptdest,
const offsettoffset 
) const
inline

Definition at line 133 of file value_set_fi.h.

◆  make_union() [1/3]

bool value_set_fit::make_union ( const value_set_fitnew_values )
inline

Definition at line 261 of file value_set_fi.h.

◆  make_union() [2/3]

bool value_set_fit::make_union ( const valuestnew_values )

Definition at line 239 of file value_set_fi.cpp.

◆  make_union() [3/3]

bool value_set_fit::make_union ( object_maptdest,
const object_maptsrc 
) const

Definition at line 277 of file value_set_fi.cpp.

◆  offset_is_zero()

bool value_set_fit::offset_is_zero ( const offsettoffset ) const
inline

Definition at line 61 of file value_set_fi.h.

◆  output()

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

Definition at line 36 of file value_set_fi.cpp.

◆  set()

void value_set_fit::set ( object_maptdest,
) const
inline

Definition at line 110 of file value_set_fi.h.

◆  set_from()

void value_set_fit::set_from ( const irep_idtfunction,
unsigned  inx 
)
inline

Definition at line 44 of file value_set_fi.h.

◆  set_to()

void value_set_fit::set_to ( const irep_idtfunction,
unsigned  inx 
)
inline

Definition at line 50 of file value_set_fi.h.

◆  to_expr()

exprt value_set_fit::to_expr ( const object_map_dt::value_typeit ) const

Definition at line 219 of file value_set_fi.cpp.

Member Data Documentation

◆  changed

bool value_set_fit::changed

Definition at line 252 of file value_set_fi.h.

◆  from_function

unsigned value_set_fit::from_function

Definition at line 39 of file value_set_fi.h.

◆  from_target_index

unsigned value_set_fit::from_target_index

Definition at line 40 of file value_set_fi.h.

◆  function_numbering

numberingt< irep_idt > value_set_fit::function_numbering
static

Definition at line 42 of file value_set_fi.h.

◆  object_numbering

object_numberingt value_set_fit::object_numbering
static

Definition at line 41 of file value_set_fi.h.

◆  to_function

unsigned value_set_fit::to_function

Definition at line 39 of file value_set_fi.h.

◆  to_target_index

unsigned value_set_fit::to_target_index

Definition at line 40 of file value_set_fi.h.

◆  values

valuest value_set_fit::values

Definition at line 250 of file value_set_fi.h.


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

AltStyle によって変換されたページ (->オリジナル) /