shadow_memory_util.cpp File Reference

Symex Shadow Memory Instrumentation Utilities. More...

#include "shadow_memory_util.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/format_expr.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/ssa_expr.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <langapi/language_util.h>
#include <pointer-analysis/value_set_dereference.h>
#include <solvers/flattening/boolbv_width.h>

Include dependency graph for shadow_memory_util.cpp:

Go to the source code of this file.

Functions
void	shadow_memory_log_set_field (const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr, const exprt &value)
	Logs setting a value to a given shadow field. More...
void	shadow_memory_log_get_field (const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr)
	Logs getting a value corresponding to a shadow memory field. More...
void	shadow_memory_log_value_set (const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set)
	Logs the retrieval of the value associated with a given shadow memory field. More...
void	shadow_memory_log_value_set_match (const namespacet &ns, const messaget &log, const exprt &address, const exprt &expr)
	Logs a successful match between an address and a value within the value set. More...
void	shadow_memory_log_text_and_expr (const namespacet &ns, const messaget &log, const char *text, const exprt &expr)
	Generic logging function that will log depending on the configured verbosity. More...
static void	log_value_set_match (const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address, const exprt &matched_base_address, const value_set_dereferencet::valuet &dereference, const exprt &expr, const value_set_dereferencet::valuet &shadow_dereference)
	Log a match between an address and the value set. More...
static void	log_try_shadow_address (const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address)
	Log trying out a match between an object and a (target) shadow address. More...
static void	log_shadow_memory_message (const messaget &log, const char *text)
	Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined. More...
static void	log_are_types_incompatible (const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address, const messaget &log)
static void	log_value_set_contains_only_null (const messaget &log, const namespacet &ns, const exprt &expr, const exprt &null_pointer)
static void	log_shadow_memory_incompatible_types (const messaget &log, const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address)
irep_idt	extract_field_name (const exprt &string_expr)
	Extracts the field name identifier from a string expression, e.g. More...
static void	remove_array_type_l2 (typet &type)
	If the given type is an array type, then remove the L2 level renaming from its size. More...
exprt	deref_expr (const exprt &expr)
	Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it just unboxes it and returns its content. More...
void	clean_pointer_expr (exprt &expr, const typet &type)
	Clean the given pointer expression so that it has the right shape for being used for identifying shadow memory. More...
void	replace_invalid_object_by_null (exprt &expr)
	Replace an invalid object by a null pointer. More...
const exprt &	get_field_init_expr (const irep_idt &field_name, const goto_symex_statet &state)
	Retrieve the expression that a field was initialised with within a given symex state. More...
const typet &	get_field_init_type (const irep_idt &field_name, const goto_symex_statet &state)
	Retrieves the type of the shadow memory by returning the type of the shadow memory initializer value. More...
bool	contains_null_or_invalid (const std::vector< exprt > &value_set, const exprt &address)
	Given a pointer expression check to see if it can be a null pointer or an invalid object within value_set. More...
static exprt	conditional_cast_floatbv_to_unsignedbv (const exprt &value)
	Casts a given (float) bitvector expression to an unsigned bitvector. More...
static void	extract_bytes_of_bv (const exprt &value, const typet &type, const typet &field_type, exprt::operandst &values)
	Extract byte-sized elements from the input bitvector-typed expression value and places them into the array values. More...
static void	extract_bytes_of_expr (exprt element, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union, exprt::operandst &values)
	Extract the components from the input expression value and places them into the array values. More...
static exprt	or_values (const exprt::operandst &values, const typet &field_type)
	Translate a list of values into an or expression. More...
exprt	compute_or_over_bytes (const exprt &expr, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union)
	Performs aggregation of the shadow memory field value over multiple bytes for fields whose type is _Bool. More...
std::pair< exprt, exprt >	compare_to_collection (const std::vector< exprt >::const_iterator &expr_iterator, const std::vector< exprt >::const_iterator &end)
	Create an expression comparing the element at expr_iterator with the following elements of the collection (or nil_exprtif none) and return a pair (condition, element) such that if the condition is true, then the element is the max of the collection in the interval denoted by expr_iterator and end. More...
static exprt	combine_condition_and_max_values (const std::vector< std::pair< exprt, exprt >> &conditions_and_values)
	Combine each (condition, value) element in the input collection into a if-then-else expression such as (cond_1 ? val_1 : (cond_2 ? val_2 : ... More...
static exprt	create_max_expr (const std::vector< exprt > &values)
	Create an expression encoding the max operation over the collection values More...
exprt	compute_max_over_bytes (const exprt &expr, const typet &field_type, const namespacet &ns)
	Performs aggregation of the shadow memory field value over multiple cells for fields whose type is a signed/unsigned bitvector (where the value is arbitrary up until the max represented by the bitvector size). More...
exprt	build_if_else_expr (const std::vector< std::pair< exprt, exprt >> &conds_values)
	Build an if-then-else chain from a vector containing pairs of expressions. More...
static bool	are_types_compatible (const typet &expr_type, const typet &shadow_type)
	Checks given types (object type and shadow memory field type) for equality. More...
static void	clean_string_constant (exprt &expr)
	Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching. More...
static void	adjust_array_types (typet &type)
	Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and pointer_type(string_constant_type) to pointer_type(char). More...
static exprt	get_matched_base_cond (const exprt &shadowed_address, const exprt &matched_base_address, const namespacet &ns, const messaget &log)
	Function that compares the two arguments shadowed_address and matched_base_address, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison. More...
static exprt	get_matched_expr_cond (const exprt &dereference_pointer, const exprt &expr, const namespacet &ns, const messaget &log)
	Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison. More...
static value_set_dereferencet::valuet	get_shadow_dereference (const exprt &shadow, const object_descriptor_exprt &matched_base_descriptor, const exprt &expr, const namespacet &ns, const messaget &log)
	Retrieve the shadow value a pointer expression may point to. More...
std::vector< std::pair< exprt, exprt > >	get_shadow_dereference_candidates (const namespacet &ns, const messaget &log, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const typet &field_type, const exprt &expr, const typet &lhs_type, bool &exact_match)
	Get a list of (condition, value) pairs for a certain pointer from the shadow memory, where each pair denotes the value of the pointer expression if the condition evaluates to true. More...
static object_descriptor_exprt	normalize (const object_descriptor_exprt &expr, const namespacet &ns)
bool	check_value_set_contains_only_null_ptr (const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set, const exprt &expr)
	Checks if value_set contains only a NULL pointer expression of the same type of expr. More...
static std::vector< std::pair< exprt, exprt > >	get_shadow_memory_for_matched_object (const exprt &expr, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, bool &exact_match)
	Used for set_field and shadow memory copy. More...
std::optional< exprt >	get_shadow_memory (const exprt &expr, const std::vector< exprt > &value_set, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, size_t &mux_size)
	Get shadow memory values for a given expression within a specified value set. More...

Detailed Description

Symex Shadow Memory Instrumentation Utilities.

Definition in file shadow_memory_util.cpp.

Function Documentation

adjust_array_types()

static void adjust_array_types ( typet &  type )

static

Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and pointer_type(string_constant_type) to pointer_type(char).

Note

type type will be changed.

Definition at line 697 of file shadow_memory_util.cpp.

are_types_compatible()

static bool are_types_compatible ( const typet &  expr_type, const typet &  shadow_type  )

static

Checks given types (object type and shadow memory field type) for equality.

We're inspecting only pointer types here - if the two types given are not pointer types, then we assume it to be vacuously true.

Parameters

expr_type	The type of the real object.
shadow_type	The type of the shadow memory field's value.

Returns

True if types equal, false otherwise.

Definition at line 651 of file shadow_memory_util.cpp.

build_if_else_expr()

exprt build_if_else_expr

(

const std::vector< std::pair< exprt, exprt >> &

conds_values

)

Build an if-then-else chain from a vector containing pairs of expressions.

Parameters

conds_values

Contains pairs <e1, e2>, where e1 is going to be used as an antecedent for an if_expr, and e2 is going to be used as the consequent.

Returns

An if_exprt of the form if e1 then e2 else if e3 then e4 else ...

Note

the expression created will not have the first condition as the first element will serve fallback if all the other conditions are false.

Definition at line 624 of file shadow_memory_util.cpp.

check_value_set_contains_only_null_ptr()

bool check_value_set_contains_only_null_ptr	(	const namespacet &	ns,
		const messaget &	log,
		const std::vector< exprt > &	value_set,
		const exprt &	expr
	)

Checks if value_set contains only a NULL pointer expression of the same type of expr.

Parameters

ns	the namespace within which we're going to perform symbol lookups
log	the message log to which we're going to print debugging messages, if debugging is set
value_set	the collection to check if it contains only the NULL pointer
expr	a pointer-typed expression

Returns

true if value_set contains only a NULL pointer expression

Definition at line 1017 of file shadow_memory_util.cpp.

clean_pointer_expr()

void clean_pointer_expr	(	exprt &	expr,
		const typet &	type
	)

Clean the given pointer expression so that it has the right shape for being used for identifying shadow memory.

This handles some quirks regarding array sizes containing L2 symbols and string constants not having char-pointer type.

Parameters

expr	The pointer to the original memory, e.g. as passed to __CPROVER_field_get.
type	The followed type of expr.

Definition at line 252 of file shadow_memory_util.cpp.

clean_string_constant()

static void clean_string_constant ( exprt &  expr )

static

Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching.

Note

expression expr will be changed.

Definition at line 682 of file shadow_memory_util.cpp.

combine_condition_and_max_values()

static exprt combine_condition_and_max_values ( const std::vector< std::pair< exprt, exprt >> &  conditions_and_values )

static

Combine each (condition, value) element in the input collection into a if-then-else expression such as (cond_1 ? val_1 : (cond_2 ? val_2 : ...

: val_n))

Parameters

conditions_and_values

collection containing codnition-value pairs

Returns

the combined max expression

Definition at line 549 of file shadow_memory_util.cpp.

compare_to_collection()

std::pair<exprt, exprt> compare_to_collection	(	const std::vector< exprt >::const_iterator &	expr_iterator,
		const std::vector< exprt >::const_iterator &	end
	)

Create an expression comparing the element at expr_iterator with the following elements of the collection (or nil_exprtif none) and return a pair (condition, element) such that if the condition is true, then the element is the max of the collection in the interval denoted by expr_iterator and end.

Parameters

expr_iterator	the iterator pointing at the element to compare to.
end	the end of collection iterator.

Returns

A pair (cond, elem) containing the condition and the max element.

Definition at line 516 of file shadow_memory_util.cpp.

compute_max_over_bytes()

exprt compute_max_over_bytes	(	const exprt &	expr,
		const typet &	field_type,
		const namespacet &	ns
	)

Performs aggregation of the shadow memory field value over multiple cells for fields whose type is a signed/unsigned bitvector (where the value is arbitrary up until the max represented by the bitvector size).

Parameters

expr	the expression to extract the max from
field_type	the type of the shadow memory field to return
ns	the namespace to perform type-lookups into

Returns

the aggregated max byte-sized value contained in expr Note that the expr type size must be known at compile time.

Definition at line 593 of file shadow_memory_util.cpp.

compute_or_over_bytes()

exprt compute_or_over_bytes	(	const exprt &	expr,
		const typet &	field_type,
		const namespacet &	ns,
		const messaget &	log,
		const bool	is_union
	)

Performs aggregation of the shadow memory field value over multiple bytes for fields whose type is _Bool.

Parameters

expr	the type to compute the or over each of its bytes
field_type	the type of the shadow memory (must be c_bool or bool)
ns	the namespace within which we're going to perform symbol lookups
log	the message log to which we're going to print debugging messages, if debugging is set
is_union	true if the expression expr is part of a union.

Returns

the aggregated or byte-sized value contained in expr

Definition at line 440 of file shadow_memory_util.cpp.

conditional_cast_floatbv_to_unsignedbv()

static exprt conditional_cast_floatbv_to_unsignedbv ( const exprt &  value )

static

Casts a given (float) bitvector expression to an unsigned bitvector.

Parameters

value

The expression that we are to conditionally cast.

Returns

An unsigned bitvector expression if eligible - id otherwise.

Definition at line 348 of file shadow_memory_util.cpp.

contains_null_or_invalid()

bool contains_null_or_invalid	(	const std::vector< exprt > &	value_set,
		const exprt &	address
	)

Given a pointer expression check to see if it can be a null pointer or an invalid object within value_set.

Parameters

address	A pointer expressions that we are using as the query.
value_set	The search space for the query.

Returns

true if the object can be null or invalid in the value set, false otherwise.

Definition at line 317 of file shadow_memory_util.cpp.

create_max_expr()

static exprt create_max_expr ( const std::vector< exprt > &  values )

static

Create an expression encoding the max operation over the collection values

Parameters

values

an exprt that encodes the max of values

Returns

an exprt encoding the max operation over the collection values

Definition at line 579 of file shadow_memory_util.cpp.

deref_expr()

exprt deref_expr

(

const exprt &

expr

)

Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it just unboxes it and returns its content.

Definition at line 242 of file shadow_memory_util.cpp.

extract_bytes_of_bv()

static void extract_bytes_of_bv ( const exprt &  value, const typet &  type, const typet &  field_type, exprt::operandst &  values  )

static

Extract byte-sized elements from the input bitvector-typed expression value and places them into the array values.

Parameters

value	the bitvector typed expression to extract the bytes from
type	the type of the expression expr (it must be bitvector)
field_type	the type of the shadow memory
values	the vector where all the extracted bytes of value will be placed.

Definition at line 367 of file shadow_memory_util.cpp.

extract_bytes_of_expr()

static void extract_bytes_of_expr ( exprt  element, const typet &  field_type, const namespacet &  ns, const messaget &  log, const bool  is_union, exprt::operandst &  values  )

static

Extract the components from the input expression value and places them into the array values.

Parameters

element	the expression to extract the bytes from
field_type	the type of the shadow memory
ns	the namespace within which we're going to perform symbol lookups
log	the message log to which we're going to print debugging messages, if debugging is set
is_union	true if the expression element is part of a union
values	the vector where all the extracted components of element will be placed.

Definition at line 396 of file shadow_memory_util.cpp.

extract_field_name()

irep_idt extract_field_name

(

const exprt &

string_expr

)

Extracts the field name identifier from a string expression, e.g.

as passed as argument to a __CPROVER_field_decl_local call.

Parameters

string_expr

The string argument expression

Returns

The identifier denoted by the string argument expression

Definition at line 212 of file shadow_memory_util.cpp.

get_field_init_expr()

const exprt& get_field_init_expr	(	const irep_idt &	field_name,
		const goto_symex_statet &	state
	)

Retrieve the expression that a field was initialised with within a given symex state.

Parameters

field_name	The field whose initialisation expression we want to retrieve.
state	The goto symex state within which we want to search for the expression.

Returns

The expression the field was initialised with.

Definition at line 298 of file shadow_memory_util.cpp.

get_field_init_type()

const typet& get_field_init_type	(	const irep_idt &	field_name,
		const goto_symex_statet &	state
	)

Retrieves the type of the shadow memory by returning the type of the shadow memory initializer value.

Parameters

field_name	The name of the field whose value type we want to query.
state	The symex_state within which the query is executed (the field's value is looked up).

Returns

The type of the value the field was initialised with (actually, the type of the value the field currently is associated with, but it's invariant since the declaration).

Definition at line 311 of file shadow_memory_util.cpp.

get_matched_base_cond()

static exprt get_matched_base_cond ( const exprt &  shadowed_address, const exprt &  matched_base_address, const namespacet &  ns, const messaget &  log  )

static

Function that compares the two arguments shadowed_address and matched_base_address, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison.

Returns

the comparison expression of shadowed_address and matched_base_address (or a true_exprt if identical modulo simplification).

Definition at line 722 of file shadow_memory_util.cpp.

get_matched_expr_cond()

static exprt get_matched_expr_cond ( const exprt &  dereference_pointer, const exprt &  expr, const namespacet &  ns, const messaget &  log  )

static

Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison.

Returns

the comparison expression of dereference_pointer and expr (or a true_exprt if identical modulo simplification).

Definition at line 761 of file shadow_memory_util.cpp.

get_shadow_dereference()

static value_set_dereferencet::valuet get_shadow_dereference ( const exprt &  shadow, const object_descriptor_exprt &  matched_base_descriptor, const exprt &  expr, const namespacet &  ns, const messaget &  log  )

static

Retrieve the shadow value a pointer expression may point to.

Parameters

shadow	The shadow expression.
matched_base_descriptor	The base descriptor for the shadow object.
expr	The pointer expression.
ns	The namespace within which we're going to perform symbol lookups.
log	The message log to which we're going to print debugging messages, if debugging is set.

Returns

A valuet object denoting the dereferenced object within shadow memory, guarded by a appropriate condition (of the form pointer == &shadow_object).

Definition at line 804 of file shadow_memory_util.cpp.

get_shadow_dereference_candidates()

std::vector<std::pair<exprt, exprt> > get_shadow_dereference_candidates	(	const namespacet &	ns,
		const messaget &	log,
		const exprt &	matched_object,
		const std::vector< shadow_memory_statet::shadowed_addresst > &	addresses,
		const typet &	field_type,
		const exprt &	expr,
		const typet &	lhs_type,
		bool &	exact_match
	)

Get a list of (condition, value) pairs for a certain pointer from the shadow memory, where each pair denotes the value of the pointer expression if the condition evaluates to true.

Returns

A vector of pair<expr, expr> corresponding to a condition and value. (See above for explanation).

Definition at line 843 of file shadow_memory_util.cpp.

get_shadow_memory()

std::optional<exprt> get_shadow_memory	(	const exprt &	expr,
		const std::vector< exprt > &	value_set,
		const std::vector< shadow_memory_statet::shadowed_addresst > &	addresses,
		const namespacet &	ns,
		const messaget &	log,
		size_t &	mux_size
	)

Get shadow memory values for a given expression within a specified value set.

Returns

if potential values are present for that object inside the value set, then we get back an if e1 then e2 else (if e3 else e4... expression, where e1, e3, ... are guards (conditions) and e2, e4, etc are the possible values of the object within the value set.

Definition at line 1130 of file shadow_memory_util.cpp.

get_shadow_memory_for_matched_object()

static std::vector<std::pair<exprt, exprt> > get_shadow_memory_for_matched_object ( const exprt &  expr, const exprt &  matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &  addresses, const namespacet &  ns, const messaget &  log, bool &  exact_match  )

static

Used for set_field and shadow memory copy.

Definition at line 1038 of file shadow_memory_util.cpp.

log_are_types_incompatible()

static void log_are_types_incompatible ( const namespacet &  ns, const exprt &  expr, const shadow_memory_statet::shadowed_addresst &  shadowed_address, const messaget &  log  )

static

Definition at line 167 of file shadow_memory_util.cpp.

log_shadow_memory_incompatible_types()

static void log_shadow_memory_incompatible_types ( const messaget &  log, const namespacet &  ns, const exprt &  expr, const shadow_memory_statet::shadowed_addresst &  shadowed_address  )

static

Definition at line 198 of file shadow_memory_util.cpp.

log_shadow_memory_message()

static void log_shadow_memory_message ( const messaget &  log, const char *  text  )

static

Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined.

Definition at line 160 of file shadow_memory_util.cpp.

log_try_shadow_address()

static void log_try_shadow_address ( const namespacet &  ns, const messaget &  log, const shadow_memory_statet::shadowed_addresst &  shadowed_address  )

static

Log trying out a match between an object and a (target) shadow address.

Definition at line 145 of file shadow_memory_util.cpp.

log_value_set_contains_only_null()

static void log_value_set_contains_only_null ( const messaget &  log, const namespacet &  ns, const exprt &  expr, const exprt &  null_pointer  )

static

Definition at line 181 of file shadow_memory_util.cpp.

log_value_set_match()

static void log_value_set_match ( const namespacet &  ns, const messaget &  log, const shadow_memory_statet::shadowed_addresst &  shadowed_address, const exprt &  matched_base_address, const value_set_dereferencet::valuet &  dereference, const exprt &  expr, const value_set_dereferencet::valuet &  shadow_dereference  )

static

Log a match between an address and the value set.

This version of the function reports more details, including the base address, the pointer and the shadow value.

Definition at line 113 of file shadow_memory_util.cpp.

normalize()

static object_descriptor_exprt normalize ( const object_descriptor_exprt &  expr, const namespacet &  ns  )

static

Definition at line 971 of file shadow_memory_util.cpp.

or_values()

static exprt or_values ( const exprt::operandst &  values, const typet &  field_type  )

static

Translate a list of values into an or expression.

Used here in the implementation of aggregation of boolean-typed fields.

Parameters

field_type	The type of the values of the or expression (expected to be the same).
values	A list (std::vector) of values collected previously, passed through immediately to the constructed expression as operands.

Returns

A newly constructed or_exprt over the possible values given.

Definition at line 431 of file shadow_memory_util.cpp.

remove_array_type_l2()

static void remove_array_type_l2 ( typet &  type )

static

If the given type is an array type, then remove the L2 level renaming from its size.

Parameters

type	Type to be modified

Definition at line 233 of file shadow_memory_util.cpp.

replace_invalid_object_by_null()

void replace_invalid_object_by_null

(

exprt &

expr

)

Replace an invalid object by a null pointer.

Works recursively on the operands (child nodes) of the expression, as well.

Parameters

expr	The (root) expression where substitution will happen.

Definition at line 279 of file shadow_memory_util.cpp.

shadow_memory_log_get_field()

void shadow_memory_log_get_field	(	const namespacet &	ns,
		const messaget &	log,
		const irep_idt &	field_name,
		const exprt &	expr
	)

Logs getting a value corresponding to a shadow memory field.

Mainly used for debugging purposes.

Definition at line 48 of file shadow_memory_util.cpp.

shadow_memory_log_set_field()

void shadow_memory_log_set_field	(	const namespacet &	ns,
		const messaget &	log,
		const irep_idt &	field_name,
		const exprt &	expr,
		const exprt &	value
	)

Logs setting a value to a given shadow field.

Mainly for use for debugging purposes.

Definition at line 31 of file shadow_memory_util.cpp.

shadow_memory_log_text_and_expr()

void shadow_memory_log_text_and_expr	(	const namespacet &	ns,
		const messaget &	log,
		const char *	text,
		const exprt &	expr
	)

Generic logging function that will log depending on the configured verbosity.

The log will be a specific message given to it, along with an expression passed along to it.

Definition at line 95 of file shadow_memory_util.cpp.

shadow_memory_log_value_set()

void shadow_memory_log_value_set	(	const namespacet &	ns,
		const messaget &	log,
		const std::vector< exprt > &	value_set
	)

Logs the retrieval of the value associated with a given shadow memory field.

Mainly for use for debugging purposes. Dual to shadow_memory_log_get_field.

Definition at line 63 of file shadow_memory_util.cpp.

shadow_memory_log_value_set_match()

void shadow_memory_log_value_set_match	(	const namespacet &	ns,
		const messaget &	log,
		const exprt &	address,
		const exprt &	expr
	)

Logs a successful match between an address and a value within the value set.

Definition at line 79 of file shadow_memory_util.cpp.