expr_initializer.h File Reference

#include "optional.h"

Include dependency graph for expr_initializer.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
optionalt< exprt >	zero_initializer (const typet &, const source_locationt &, const namespacet &)
	Create the equivalent of zero for type type. More...
optionalt< 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. More...

Detailed Description

Expression Initialization

Definition in file expr_initializer.h.

Function Documentation

nondet_initializer()

optionalt<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 312 of file expr_initializer.cpp.

zero_initializer()

optionalt<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 297 of file expr_initializer.cpp.