cprover
value_sett Class Reference

State type in value_set_domaint, used in value-set analysis and goto-symex. More...

#include <value_set.h>

+ Collaboration diagram for value_sett:

Classes

struct  entryt
 Represents a row of a value_sett. More...
 
class  object_map_dt
 Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances). More...
 

Public Types

enum  insert_actiont { insert_actiont::INSERT, insert_actiont::RESET_OFFSET, insert_actiont::NONE }
 
typedef optionalt< mp_integeroffsett
 Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset. More...
 
typedef reference_counting< object_map_dtobject_mapt
 Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances can share them. More...
 
typedef std::set< exprtexpr_sett
 Set of expressions; only used for the get API, not for internal data representation. More...
 
typedef std::set< unsigned int > dynamic_object_id_sett
 Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs. More...
 
typedef sharing_mapt< irep_idt, entrytvaluest
 Map representing the entire value set, mapping from string LHS IDs to RHS expression sets. More...
 

Public Member Functions

 value_sett ()
 
 value_sett (value_sett &&other)
 
virtual ~value_sett ()=default
 
 value_sett (const value_sett &other)=default
 
value_settoperator= (const value_sett &other)=delete
 
value_settoperator= (value_sett &&other)
 
virtual bool field_sensitive (const irep_idt &id, const typet &type)
 Determines whether an identifier of a given type should have its fields distinguished. More...
 
bool offset_is_zero (const offsett &offset) const
 
exprt to_expr (const object_map_dt::value_type &it) const
 Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with .object() == object_numbering.at(object_number) and .offset() == offset. More...
 
void set (object_mapt &dest, const object_map_dt::value_type &it) const
 Sets an element in object map dest to match an existing element it from a different map. More...
 
bool insert (object_mapt &dest, const object_map_dt::value_type &it) const
 Merges an existing element into an object map. More...
 
bool insert (object_mapt &dest, const exprt &src) const
 Adds an expression to an object map, with unknown offset. More...
 
bool insert (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
 Adds an expression to an object map, with known offset. More...
 
bool insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
 Adds a numbered expression and offset to an object map. More...
 
insert_actiont get_insert_action (const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
 Determines what would happen if object number n was inserted into map dest with offset offset – the possibilities being, nothing (the entry is already present), a new entry would be inserted (no existing entry with number n was found), or an existing entry's offset would be reset (indicating there is already an entry with number n, but with differing offset). More...
 
bool insert (object_mapt &dest, const exprt &expr, const offsett &offset) const
 Adds an expression and offset to an object map. More...
 
void get_value_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
 Gets values pointed to by expr, including following dereference operators (i.e. More...
 
expr_settget (const irep_idt &identifier, const std::string &suffix)
 Appears to be unimplemented. More...
 
void clear ()
 
const entrytfind_entry (const irep_idt &id) const
 Finds an entry in this value-set. More...
 
void update_entry (const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)
 Adds or replaces an entry in this value-set. More...
 
void output (const namespacet &ns, std::ostream &out) const
 Pretty-print this value-set. More...
 
bool make_union (object_mapt &dest, const object_mapt &src) const
 Merges two RHS expression sets. More...
 
bool make_union_would_change (const object_mapt &dest, const object_mapt &src) const
 Determines whether merging two RHS expression sets would cause any change. More...
 
bool make_union (const valuest &new_values)
 Merges an entire existing value_sett's data into this one. More...
 
bool make_union (const value_sett &new_values)
 Merges an entire existing value_sett's data into this one. More...
 
void guard (const exprt &expr, const namespacet &ns)
 Transforms this value-set by assuming an expression holds. More...
 
void apply_code (const codet &code, const namespacet &ns)
 Transforms this value-set by executing a given statement against it. More...
 
void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
 Transforms this value-set by executing executing the assignment lhs := rhs against it. More...
 
void do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
 Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee. More...
 
void do_end_function (const exprt &lhs, const namespacet &ns)
 Transforms this value-set by assigning this function's return value to a given LHS expression. More...
 
void get_reference_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
 Gets the set of expressions that expr may refer to, according to this value set. More...
 
bool eval_pointer_offset (exprt &expr, const namespacet &ns) const
 Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-set's information. More...
 
optionalt< irep_idtget_index_of_symbol (irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
 Get the index of the symbol and suffix. More...
 
void erase_values_from_entry (const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
 Update the entry stored at index by erasing any values listed in values_to_erase. More...
 
void erase_symbol (const symbol_exprt &symbol_expr, const namespacet &ns)
 

Public Attributes

unsigned location_number
 Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map. More...
 
valuest values
 Stores the LHS ID -> RHS expression set map. More...
 

Static Public Attributes

static object_numberingt object_numbering
 Global shared object numbering, used to abbreviate expressions stored in value sets. More...
 

Protected Member Functions

void get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns, bool is_simplified) const
 Reads the set of objects pointed to by expr, including making recursive lookups for dereference operations etc. More...
 
void get_reference_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 See the other overload of get_reference_set. More...
 
void get_reference_set_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const
 See get_reference_set. More...
 
void dereference_rec (const exprt &src, exprt &dest) const
 Sets dest to src with any wrapping typecasts removed. More...
 
void erase_symbol_rec (const typet &type, const std::string &erase_prefix, const namespacet &ns)
 
void erase_struct_union_symbol (const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
 
virtual void get_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
 Subclass customisation point for recursion over RHS expression: More...
 
virtual void assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
 Subclass customisation point for recursion over LHS expression: More...
 
virtual void apply_code_rec (const codet &code, const namespacet &ns)
 Subclass customisation point for applying code to this domain: More...
 

Private Member Functions

virtual void adjust_assign_rhs_values (const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
 Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign. More...
 
virtual void apply_assign_side_effects (const exprt &lhs, const exprt &rhs, const namespacet &)
 Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written. More...
 

Detailed Description

State type in value_set_domaint, used in value-set analysis and goto-symex.

Represents a mapping from expressions to the addresses that may be stored there; for example, a global that is either null or points to a heap-allocated object, which itself has two fields, one pointing to another heap object and the other having unknown target, would be represented:

global_x -> { null, <dynamic_object1, 0> }
dynamic_object1.field1 -> { <dynamic_object2, 0> }
dynamic_object1.field2 -> { * (unknown) }

LHS expressions can be either symbols or fields thereof, and are stored as strings; RHS expressions may be symbols, dynamic objects, integer addresses (as in (int*)0x1234) or unknown (printed as *), and are stored as pairs of an exprt and an optional offset if known (0 for both dynamic objects in the example given above). RHS expressions are represented using numbering to avoid storing redundant duplicate expressions.

Definition at line 44 of file value_set.h.

Member Typedef Documentation

◆ dynamic_object_id_sett

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

Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs.

Used only in internal implementation details.

Definition at line 305 of file value_set.h.

◆ expr_sett

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

Set of expressions; only used for the get API, not for internal data representation.

Definition at line 300 of file value_set.h.

◆ object_mapt

Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances can share them.

For example, if we have a pair of instructions with value-sets:

x = new A;
  x -> { dynamic_object1 }
y = new B;
  x -> { dynamic_object1 }
  y -> { dynamic_object2 }

Then the set { dynamic_object1 }, represented by an object_map_dt, can be shared between the two value_sett instances.

Definition at line 178 of file value_set.h.

◆ offsett

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

Definition at line 82 of file value_set.h.

◆ valuest

Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.

Note this data structure is somewhat denormalized, for example mapping

dynamic_object1.field2 ->
    entryt {
     .identifier = dynamic_object1,
     .suffix = .field2,
     .object_map = ...
    }

The components of the ID are thus duplicated in the valuest key and in entryt fields.

Definition at line 320 of file value_set.h.

Member Enumeration Documentation

◆ insert_actiont

Enumerator
INSERT 
RESET_OFFSET 
NONE 

Definition at line 237 of file value_set.h.

Constructor & Destructor Documentation

◆ value_sett() [1/3]

value_sett::value_sett ( )
inline

Definition at line 47 of file value_set.h.

◆ value_sett() [2/3]

value_sett::value_sett ( value_sett &&  other)
inline

Definition at line 51 of file value_set.h.

◆ ~value_sett()

virtual value_sett::~value_sett ( )
virtualdefault

◆ value_sett() [3/3]

value_sett::value_sett ( const value_sett other)
default

Member Function Documentation

◆ adjust_assign_rhs_values()

virtual void value_sett::adjust_assign_rhs_values ( const exprt rhs,
const namespacet ,
object_mapt rhs_values 
) const
inlineprivatevirtual

Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign.

For example, this is used in one subclass to tag and thus differentiate values that originated in a particular place, vs. those that have been copied.

Definition at line 588 of file value_set.h.

◆ apply_assign_side_effects()

virtual void value_sett::apply_assign_side_effects ( const exprt lhs,
const exprt rhs,
const namespacet  
)
inlineprivatevirtual

Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written.

For example, this is used in a recency-analysis plugin to demote existing most-recent objects to general case ones.

Definition at line 602 of file value_set.h.

◆ apply_code()

void value_sett::apply_code ( const codet code,
const namespacet ns 
)
inline

Transforms this value-set by executing a given statement against it.

For example, assignment statements will update valuest by reading the value-set corresponding to their right-hand side and assigning it to their LHS.

Parameters
codeinstruction to apply
nsglobal namespace

Definition at line 417 of file value_set.h.

◆ apply_code_rec()

void value_sett::apply_code_rec ( const codet code,
const namespacet ns 
)
protectedvirtual

Subclass customisation point for applying code to this domain:

Definition at line 1507 of file value_set.cpp.

◆ assign()

void value_sett::assign ( const exprt lhs,
const exprt rhs,
const namespacet ns,
bool  is_simplified,
bool  add_to_sets 
)

Transforms this value-set by executing executing the assignment lhs := rhs against it.

Parameters
lhswritten expression
rhsread expression
nsglobal namespace
is_simplifiedif false, simplify will be used to simplify RHS and LHS before execution. If you know they are already simplified, set this to save a little time.
add_to_setsif true, execute a weak assignment (the LHS possible values are added to but not overwritten). Otherwise execute a strong (overwriting) assignment. Note the nature of lhs may internally prevent a strong assignment, as in x == y ? z : w := a, where either y or z MAY, but not MUST, be overwritten.

Definition at line 1189 of file value_set.cpp.

◆ assign_rec()

void value_sett::assign_rec ( const exprt lhs,
const object_mapt values_rhs,
const std::string &  suffix,
const namespacet ns,
bool  add_to_sets 
)
protectedvirtual

Subclass customisation point for recursion over LHS expression:

Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.

Definition at line 1320 of file value_set.cpp.

◆ clear()

void value_sett::clear ( void  )
inline

Definition at line 335 of file value_set.h.

◆ dereference_rec()

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

Sets dest to src with any wrapping typecasts removed.

Definition at line 995 of file value_set.cpp.

◆ do_end_function()

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

Transforms this value-set by assigning this function's return value to a given LHS expression.

Note this has no effect if remove_returns has been run, in which case returns are explicitly passed via global variables named function_name::return_value and are handled via the usual apply_code path.

Parameters
lhsexpression that receives the return value
nsglobal namespace

Definition at line 1495 of file value_set.cpp.

◆ do_function_call()

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

Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee.

For example, for function f(int* x, void* y) and call f(&g, &h) this would execute assignments x := &g and y := &h.

Parameters
functionfunction being called
argumentsactual arguments
nsglobal namespace

Definition at line 1449 of file value_set.cpp.

◆ erase_struct_union_symbol()

void value_sett::erase_struct_union_symbol ( const struct_union_typet struct_union_type,
const std::string &  erase_prefix,
const namespacet ns 
)
protected

Definition at line 1698 of file value_set.cpp.

◆ erase_symbol()

void value_sett::erase_symbol ( const symbol_exprt symbol_expr,
const namespacet ns 
)

Definition at line 1733 of file value_set.cpp.

◆ erase_symbol_rec()

void value_sett::erase_symbol_rec ( const typet type,
const std::string &  erase_prefix,
const namespacet ns 
)
protected

Definition at line 1716 of file value_set.cpp.

◆ erase_values_from_entry()

void value_sett::erase_values_from_entry ( const irep_idt index,
const std::unordered_set< exprt, irep_hash > &  values_to_erase 
)

Update the entry stored at index by erasing any values listed in values_to_erase.

Parameters
indexindex in the value set
values_to_eraseset of values to remove from the entry

Definition at line 1663 of file value_set.cpp.

◆ eval_pointer_offset()

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

Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-set's information.

For example, if expr contained POINTER_OFFSET(y), and this value set indicates y points to object z offset 4, then the expression will be replaced by constant 4. If we don't know where y points, or it may point to multiple distinct offsets, then the expression will be left alone.

Parameters
exprexpression whose pointer offsets should be replaced
nsglobal namespace
Returns
true if any offset expression was successfully replaced.

Definition at line 300 of file value_set.cpp.

◆ field_sensitive()

bool value_sett::field_sensitive ( const irep_idt id,
const typet type 
)
virtual

Determines whether an identifier of a given type should have its fields distinguished.

Virtual so that subclasses can override this behaviour.

Definition at line 39 of file value_set.cpp.

◆ find_entry()

const value_sett::entryt * value_sett::find_entry ( const irep_idt id) const

Finds an entry in this value-set.

The interface differs from update_entry because get_value_set_rec wants to check for a struct's first component before stripping the suffix as is done in update_entry.

Parameters
ididentifier to find.
Returns
a constant pointer to an entry if found, or null otherwise.

Definition at line 51 of file value_set.cpp.

◆ get()

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

Appears to be unimplemented.

◆ get_index_of_symbol()

optionalt< irep_idt > value_sett::get_index_of_symbol ( irep_idt  identifier,
const typet type,
const std::string &  suffix,
const namespacet ns 
) const

Get the index of the symbol and suffix.

Parameters
identifierThe identifier for the symbol
typeThe type of the symbol
suffixThe suffix for the entry
nsThe global namespace, for following type if it is a struct tag type or a union tag type
Returns
The index if the symbol is known, else nullopt.

Definition at line 411 of file value_set.cpp.

◆ get_insert_action()

value_sett::insert_actiont value_sett::get_insert_action ( const object_mapt dest,
object_numberingt::number_type  n,
const offsett offset 
) const

Determines what would happen if object number n was inserted into map dest with offset offset – the possibilities being, nothing (the entry is already present), a new entry would be inserted (no existing entry with number n was found), or an existing entry's offset would be reset (indicating there is already an entry with number n, but with differing offset).

Definition at line 96 of file value_set.cpp.

◆ get_reference_set() [1/2]

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

Gets the set of expressions that expr may refer to, according to this value set.

Note the contrast with get_value_set: if x holds a pointer to y, then get_value_set(x) includes y while get_reference_set(x) returns { x }.

Parameters
exprquery expression
[out]destoverwritten with result expression set
nsglobal namespace

Definition at line 1013 of file value_set.cpp.

◆ get_reference_set() [2/2]

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

See the other overload of get_reference_set.

This one returns object numbers and offsets instead of expressions.

Definition at line 530 of file value_set.h.

◆ get_reference_set_rec()

void value_sett::get_reference_set_rec ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
protected

See get_reference_set.

Definition at line 1028 of file value_set.cpp.

◆ get_value_set() [1/2]

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

Gets values pointed to by expr, including following dereference operators (i.e.

this is not a simple lookup in valuest).

Parameters
exprquery expression
[out]destassigned a set of expressions that expr may point to
nsglobal namespace

Definition at line 353 of file value_set.cpp.

◆ 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

Reads the set of objects pointed to by expr, including making recursive lookups for dereference operations etc.

Parameters
exprquery expression
[out]destoverwritten by the set of object numbers pointed to
nsglobal namespace
is_simplifiedif false, simplify expr before reading.

Definition at line 374 of file value_set.cpp.

◆ get_value_set_rec()

void value_sett::get_value_set_rec ( const exprt expr,
object_mapt dest,
const std::string &  suffix,
const typet original_type,
const namespacet ns 
) const
protectedvirtual

Subclass customisation point for recursion over RHS expression:

Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.

Definition at line 462 of file value_set.cpp.

◆ guard()

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

Transforms this value-set by assuming an expression holds.

Currently this can only mark dynamic objects valid; all other assumptions are ignored.

Parameters
exprcondition to assume
nsglobal namespace

Definition at line 1629 of file value_set.cpp.

◆ insert() [1/5]

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

Merges an existing element into an object map.

If the destination map has an existing element for the same expression with a different offset its offset is marked unknown (so e.g. x -> 0 and x -> 1 merge into x -> ?).

Parameters
destobject map to update.
ititerator pointing to new element

Definition at line 196 of file value_set.h.

◆ insert() [2/5]

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

Adds an expression to an object map, with unknown offset.

If the destination map has an existing element for the same expression its offset is marked unknown.

Parameters
destobject map to update
srcexpression to add

Definition at line 206 of file value_set.h.

◆ insert() [3/5]

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

Adds an expression to an object map, with known offset.

If the destination map has an existing element for the same expression with a differing offset its offset is marked unknown.

Parameters
destobject map to update
srcexpression to add
offset_valueoffset into src

Definition at line 217 of file value_set.h.

◆ insert() [4/5]

bool value_sett::insert ( object_mapt dest,
object_numberingt::number_type  n,
const offsett offset 
) const

Adds a numbered expression and offset to an object map.

If the destination map has an existing element for the same expression with a differing offset its offset is marked unknown.

Parameters
destobject map to update
nobject number to add; must be mapped to the corresponding expression by object_numbering.
offsetoffset into object n (may be unknown).

Definition at line 116 of file value_set.cpp.

◆ insert() [5/5]

bool value_sett::insert ( object_mapt dest,
const exprt expr,
const offsett offset 
) const
inline

Adds an expression and offset to an object map.

If the destination map has an existing element for the same expression with a differing offset its offset is marked unknown.

Parameters
destobject map to update
exprexpression to add
offsetoffset into expr (may be unknown).

Definition at line 261 of file value_set.h.

◆ make_union() [1/3]

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

Merges two RHS expression sets.

Parameters
[in,out]destset to merge into
srcset to merge in
Returns
true if anything changed.

Definition at line 285 of file value_set.cpp.

◆ make_union() [2/3]

bool value_sett::make_union ( const valuest new_values)

Merges an entire existing value_sett's data into this one.

Parameters
new_valuesnew values to merge in
Returns
true if anything changed.

Definition at line 235 of file value_set.cpp.

◆ make_union() [3/3]

bool value_sett::make_union ( const value_sett new_values)
inline

Merges an entire existing value_sett's data into this one.

Returns
true if anything changed.

Definition at line 397 of file value_set.h.

◆ make_union_would_change()

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

Determines whether merging two RHS expression sets would cause any change.

Parameters
destset that would be merged into
srcset that would be merged in
Returns
true if anything changed.

Definition at line 267 of file value_set.cpp.

◆ offset_is_zero()

bool value_sett::offset_is_zero ( const offsett offset) const
inline

Definition at line 83 of file value_set.h.

◆ operator=() [1/2]

value_sett& value_sett::operator= ( const value_sett other)
delete

◆ operator=() [2/2]

value_sett& value_sett::operator= ( value_sett &&  other)
inline

Definition at line 62 of file value_set.h.

◆ output()

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

Pretty-print this value-set.

Parameters
nsglobal namespace
[out]outstream to write to

Definition at line 134 of file value_set.cpp.

◆ set()

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

Sets an element in object map dest to match an existing element it from a different map.

Any existing element for the same exprt is overwritten.

Parameters
destobject map to update.
ititerator pointing to new element

Definition at line 185 of file value_set.h.

◆ to_expr()

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

Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with .object() == object_numbering.at(object_number) and .offset() == offset.

Definition at line 215 of file value_set.cpp.

◆ update_entry()

void value_sett::update_entry ( const entryt e,
const typet type,
const object_mapt new_values,
bool  add_to_sets 
)

Adds or replaces an entry in this value-set.

Parameters
eentry to find. Its id and suffix fields will be used to find a corresponding entry; if a fresh entry is created its object_map (RHS value set) will be merged with or replaced by new_values, depending on the value of add_to_sets. If an entry already exists, the object map of e is ignored.
typetype of e.identifier, used to determine whether e's suffix should be used to find a field-sensitive value-set or whether a single entry should be shared by all of symbol e.identifier.
new_valuesvalues to be stored for the entry.
add_to_setsif true, merge in new_values instead of replacing the existing values.

Definition at line 57 of file value_set.cpp.

Member Data Documentation

◆ location_number

unsigned value_sett::location_number

Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map.

Definition at line 74 of file value_set.h.

◆ object_numbering

object_numberingt value_sett::object_numbering
static

Global shared object numbering, used to abbreviate expressions stored in value sets.

Definition at line 78 of file value_set.h.

◆ values

valuest value_sett::values

Stores the LHS ID -> RHS expression set map.

See valuest documentation for more detail.

Definition at line 375 of file value_set.h.


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