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...

Public Types
enum class	insert_actiont { INSERT , RESET_OFFSET , NONE }

typedef std::optional< mp_integer >	offsett
	Represents the offset into an object: either a unique integer offset, or an unknown value, represented by `!offset`. More...

using	object_map_dt = std::map< object_numberingt::number_type, offsett >
	Represents a set of expressions (`exprt` instances) with corresponding offsets (`offsett` instances). More...

using	object_mapt = reference_counting< object_map_dt, empty_object_map >
	Reference-counts instances of `object_map_dt`, such that multiple instructions' `value_sett` instances can share them. More...

typedef sharing_mapt< irep_idt, entryt >	valuest
	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_sett &	operator= (const value_sett &other)=delete

value_sett &	operator= (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...

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...

std::vector< exprt >	get_value_set (exprt expr, const namespacet &ns) const
	Gets values pointed to by `expr`, including following dereference operators (i.e. More...

void	clear ()

const entryt *	find_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 (std::ostream &out, const std::string &indent="") const
	Pretty-print this value-set. More...

xmlt	output_xml (void) const
	Output the value set formatted as XML. 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...

std::optional< irep_idt >	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. 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...

static const object_map_dt	empty_object_map {}

Protected Member Functions
object_mapt	get_value_set (exprt expr, 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, bool &includes_nondet_pointer, 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 43 of file value_set.h.

Member Typedef Documentation

◆ object_map_dt

using value_sett::object_map_dt = std::map<object_numberingt::number_type, offsett>

Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).

This is the RHS set of a single row of the enclosing value_sett, such as { null, dynamic_object1 }. The set is represented as a map from numbered exprts to offsett instead of a set of pairs to make lookup by exprt easier.

Definition at line 88 of file value_set.h.

◆ object_mapt

using value_sett::object_mapt = reference_counting<object_map_dt, empty_object_map>

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 110 of file value_set.h.

◆ offsett

typedef std::optional<mp_integer> value_sett::offsett

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

Definition at line 81 of file value_set.h.

◆ valuest

typedef sharing_mapt<irep_idt, entryt> value_sett::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 245 of file value_set.h.

Member Enumeration Documentation

◆ insert_actiont

enum value_sett::insert_actiont

strong

Enumerator
INSERT
RESET_OFFSET
NONE

Definition at line 169 of file value_set.h.

Constructor & Destructor Documentation

◆ value_sett() [1/3]

value_sett::value_sett ( )

inline

Definition at line 46 of file value_set.h.

◆ value_sett() [2/3]

value_sett::value_sett ( value_sett && other )

inline

Definition at line 50 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 514 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 528 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

code	instruction to apply
ns	global namespace

Definition at line 338 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 1829 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

lhs	written expression
rhs	read expression
ns	global namespace
is_simplified	if 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_sets	if 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 1486 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 1641 of file value_set.cpp.

◆ clear()

void value_sett::clear ( void )

inline

Definition at line 255 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 1291 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

lhs	expression that receives the return value
ns	global namespace

Definition at line 1817 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

function	function being called
arguments	actual arguments
ns	global namespace

Definition at line 1771 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 2021 of file value_set.cpp.

◆ erase_symbol()

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

Definition at line 2059 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 2041 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

index	index in the value set
values_to_erase	set of values to remove from the entry

Definition at line 1986 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

expr	expression whose pointer offsets should be replaced
ns	global namespace

Returns: true if any offset expression was successfully replaced.

Definition at line 338 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 46 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

id	identifier to find.

Returns: a constant pointer to an entry if found, or null otherwise.

Definition at line 58 of file value_set.cpp.

◆ get_index_of_symbol()

std::optional< 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

identifier	The identifier for the symbol
type	The type of the symbol
suffix	The suffix for the entry
ns	The 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 451 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 103 of file value_set.cpp.

◆ get_reference_set() [1/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 448 of file value_set.h.

◆ get_reference_set() [2/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

	expr	query expression
[out]	dest	overwritten with result expression set
	ns	global namespace

Definition at line 1306 of file value_set.cpp.

◆ 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 1321 of file value_set.cpp.

◆ get_value_set() [1/2]

std::vector< exprt > value_sett::get_value_set	(	exprt	expr,
		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

expr	query expression
ns	global namespace

Returns: list of expressions that expr may point to. These expressions are object_descriptor_exprt or have id ID_invalid or ID_unknown.

Definition at line 390 of file value_set.cpp.

◆ get_value_set() [2/2]

value_sett::object_mapt value_sett::get_value_set	(	exprt	expr,
		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

expr	query expression
ns	global namespace
is_simplified	if false, simplify `expr` before reading.

Returns: the set of object numbers pointed to

Definition at line 397 of file value_set.cpp.

◆ get_value_set_rec()

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

protectedvirtual

Subclass customisation point for recursion over RHS expression.

Parameters

	expr	RHS expression to get value set for.
[out]	dest	value set for `expr`.
[out]	includes_nondet_pointer	`expr` includes a non-deterministic value, and the caller may want to expand `dest` to reflect this.
	suffix	context to enable field sensitivity.
	original_type	type of `expr` when starting the recursion.
	ns	namespace.

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

Definition at line 505 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

expr	condition to assume
ns	global namespace

Definition at line 1954 of file value_set.cpp.

◆ insert() [1/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

dest	object map to update
expr	expression to add
offset	offset into `expr` (may be unknown).

Definition at line 193 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

dest	object map to update
src	expression to add

Definition at line 138 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

dest	object map to update
src	expression to add
offset_value	offset into `src`

Definition at line 149 of file value_set.h.

◆ insert() [4/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

dest	object map to update.
it	iterator pointing to new element

Definition at line 128 of file value_set.h.

◆ insert() [5/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

dest	object map to update
n	object number to add; must be mapped to the corresponding expression by `object_numbering`.
offset	offset into object `n` (may be unknown).

Definition at line 123 of file value_set.cpp.

◆ make_union() [1/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 318 of file value_set.h.

◆ 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_values new values to merge in

Returns: true if anything changed.

Definition at line 273 of file value_set.cpp.

◆ make_union() [3/3]

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

Merges two RHS expression sets.

Parameters

[in,out]	dest	set to merge into
	src	set to merge in

Returns: true if anything changed.

Definition at line 323 of file value_set.cpp.

◆ 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

dest	set that would be merged into
src	set that would be merged in

Returns: true if anything changed.

Definition at line 305 of file value_set.cpp.

◆ 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 61 of file value_set.h.

◆ output()

void value_sett::output	(	std::ostream &	out,
		const std::string &	indent = `""`
	)		const

Pretty-print this value-set.

Parameters

[out]	out	stream to write to
	indent	string to use for indentation of the output

Definition at line 141 of file value_set.cpp.

◆ output_xml()

xmlt value_sett::output_xml ( void ) const

Output the value set formatted as XML.

Definition at line 220 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

dest	object map to update.
it	iterator pointing to new element

Definition at line 117 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 253 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

e	entry 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.
type	type 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_values	values to be stored for the entry.
add_to_sets	if true, merge in `new_values` instead of replacing the existing values.

Definition at line 64 of file value_set.cpp.

Member Data Documentation

◆ empty_object_map

const value_sett::object_map_dt value_sett::empty_object_map {}

static

Definition at line 90 of file value_set.h.

◆ 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 73 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 77 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 296 of file value_set.h.

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

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Protected Member Functions

Private Member Functions

Detailed Description

Member Typedef Documentation

◆ object_map_dt

◆ object_mapt

◆ offsett

◆ valuest

Member Enumeration Documentation

◆ insert_actiont

Constructor & Destructor Documentation

◆ value_sett() [1/3]

◆ value_sett() [2/3]

◆ ~value_sett()

◆ value_sett() [3/3]

Member Function Documentation

◆ adjust_assign_rhs_values()

◆ apply_assign_side_effects()

◆ apply_code()

◆ apply_code_rec()

◆ assign()

◆ assign_rec()

◆ clear()

◆ dereference_rec()

◆ do_end_function()

◆ do_function_call()

◆ erase_struct_union_symbol()

◆ erase_symbol()

◆ erase_symbol_rec()

◆ erase_values_from_entry()

◆ eval_pointer_offset()

◆ field_sensitive()

◆ find_entry()

◆ get_index_of_symbol()

◆ get_insert_action()

◆ get_reference_set() [1/2]

◆ get_reference_set() [2/2]

◆ get_reference_set_rec()

◆ get_value_set() [1/2]

◆ get_value_set() [2/2]

◆ get_value_set_rec()

◆ guard()

◆ insert() [1/5]

◆ insert() [2/5]

◆ insert() [3/5]

◆ insert() [4/5]

◆ insert() [5/5]

◆ make_union() [1/3]

◆ make_union() [2/3]

◆ make_union() [3/3]

◆ make_union_would_change()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ output()

◆ output_xml()

◆ set()

◆ to_expr()

◆ update_entry()

Member Data Documentation

◆ empty_object_map

◆ location_number

◆ object_numbering

◆ values