Loading...

Searching...

No Matches

Functions

expr_initializer.h File Reference

Expression Initialization. More...

#include <optional>

+ 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

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

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.

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

Function Documentation

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