expr_initializer.cpp File Reference

Expression Initialization. More...

#include "expr_initializer.h"
#include "arith_tools.h"
#include "bitvector_expr.h"
#include "byte_operators.h"
#include "c_types.h"
#include "config.h"
#include "magic.h"
#include "namespace.h"
#include "simplify_expr.h"
#include "std_code.h"
#include "symbol_table.h"

Include dependency graph for expr_initializer.cpp:

Go to the source code of this file.

Classes
class	expr_initializert

Functions
std::optional< exprt >	zero_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns)
	Create the equivalent of zero for type type.
std::optional< exprt >	nondet_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns)
	Create a non-deterministic value for type type, with all subtypes independently expanded as non-deterministic values.
std::optional< exprt >	expr_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns, const exprt &init_byte_expr)
	Create a value for type type, with all subtype bytes initialized to the given value.
static exprt	cast_or_reinterpret (const exprt &expr, const typet &out_type)
	Typecast the input to the output if this is a signed/unsigned bv.
exprt	duplicate_per_byte (const exprt &init_byte_expr, const typet &output_type, const namespacet &ns)
	Builds an expression of the given output type with each of its bytes initialized to the given initialization expression.

Detailed Description

Expression Initialization.

Definition in file expr_initializer.cpp.

Function Documentation

cast_or_reinterpret()

static exprt cast_or_reinterpret ( const exprt &  expr, const typet &  out_type  )

static

Typecast the input to the output if this is a signed/unsigned bv.

Perform a reinterpret cast using byte_extract otherwise.

Parameters

expr	the expression to be casted if necessary.
out_type	the type to cast the expression to.

Returns

the casted or reinterpreted expression.

Definition at line 354 of file expr_initializer.cpp.

duplicate_per_byte()

exprt duplicate_per_byte	(	const exprt &	init_byte_expr,
		const typet &	output_type,
		const namespacet &	ns
	)

Builds an expression of the given output type with each of its bytes initialized to the given initialization expression.

Integer bitvector types are currently supported. For unsupported output_type the initialization expression is casted to the output type.

Parameters

init_byte_expr	The initialization expression
output_type	The output type
ns	Namespace to perform type symbol/tag lookups

Returns

The built expression

Note

init_byte_expr must be a boolean or a bitvector and must be of at most size <= config.ansi_c.char_width

Definition at line 381 of file expr_initializer.cpp.

expr_initializer()

std::optional< exprt > expr_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns,
		const exprt &	init_byte_expr
	)

Create a value for type type, with all subtype bytes initialized to the given value.

Parameters

type	Type of the target expression.
source_location	Location to record in all created sub-expressions.
ns	Namespace to perform type symbol/tag lookups.
init_byte_expr	Value to be used for initialization.

Returns

An expression if a byte-initialized expression of the input type can be built.

Definition at line 340 of file expr_initializer.cpp.

nondet_initializer()

std::optional< exprt > nondet_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns
	)

Create a non-deterministic value for type type, with all subtypes independently expanded as non-deterministic values.

Parameters

type	Type of the target expression.
source_location	Location to record in all created sub-expressions.
ns	Namespace to perform type symbol/tag lookups.

Returns

An expression if a non-deterministic expression of the input type can be built.

Definition at line 324 of file expr_initializer.cpp.

zero_initializer()

std::optional< exprt > zero_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns
	)

Create the equivalent of zero for type type.

Parameters

type	Type of the target expression.
source_location	Location to record in all created sub-expressions.
ns	Namespace to perform type symbol/tag lookups.

Returns

An expression if a constant expression of the input type can be built.

Definition at line 308 of file expr_initializer.cpp.