goto_symex_utils Namespace Reference

Functions
expr2tc	gen_byte_memcpy (const expr2tc &src, const expr2tc &dst, const size_t num_of_bytes, const size_t src_offset, const size_t dst_offset)
	Computes the equivalent object value when considering a memcpy operation on it.
bool	is_alloca_return_value_name (const std::string &name)
	Returns true iff name is the goto-program return-value temp for an alloca / __builtin_alloca call, i.e.

Function Documentation

gen_byte_memcpy()

expr2tc goto_symex_utils::gen_byte_memcpy	(	const expr2tc &	src,
		const expr2tc &	dst,
		const size_t	num_of_bytes,
		const size_t	src_offset,
		const size_t	dst_offset )

Computes the equivalent object value when considering a memcpy operation on it.

Parameters

src	The source expression from which bytes are copied.
dst	The destination expression to which bytes are copied.
num_of_bytes	The number of bytes to copy from src to dst.
src_offset	The offset in src from which the bytes start.
dst_offset	The offset in dst at which the bytes are written.

Returns

A new expr2tc representing the result of the memcpy operation, or an empty expr2tc if unable construct the object

Usage Examples:

expr2tc src = constant_int2tc(get_uint_type(32), BigInt(0xdeadbeef));
expr2tc dst = constant_int2tc(get_uint_type(32), BigInt(0x12345678));
size_t num_of_bytes = 1;
size_t src_offset = 1;
size_t dst_offset = 2;
 
expr2tc result = gen_byte_memcpy(src, dst, num_of_bytes, src_offset,
dst_offset);
// result should be constant_int2tc(bitvec_type(32)), BigInt(0x12de345678));

is_alloca_return_value_name()

bool goto_symex_utils::is_alloca_return_value_name

(

const std::string &

name

)

Returns true iff name is the goto-program return-value temp for an alloca / __builtin_alloca call, i.e.

exactly matches <L1-prefix?>return_value$_alloca$<digits> or <L1-prefix?>return_value$___builtin_alloca$<digits>. Only these allocations die with their frame; the models' __ESBMC_alloca outlives it.

A previous substring-only check fired on any user identifier containing _alloca$ (e.g. a method literally named alloca$te), causing symex to free a non-alloca'd dynamic object. See #2095.