CBMC
|
Expression Initialization. More...
#include <optional>
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 . More... | |
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. More... | |
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. More... | |
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. More... | |
Expression Initialization.
Definition in file expr_initializer.h.
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.
init_byte_expr | The initialization expression |
output_type | The output type |
ns | Namespace to perform type symbol/tag lookups |
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.
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.
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. |
Definition at line 340 of file expr_initializer.cpp.
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.
type | Type of the target expression. |
source_location | Location to record in all created sub-expressions. |
ns | Namespace to perform type symbol/tag lookups. |
Definition at line 324 of file expr_initializer.cpp.
std::optional<exprt> zero_initializer | ( | const typet & | type, |
const source_locationt & | source_location, | ||
const namespacet & | ns | ||
) |
Create the equivalent of zero for type type
.
type | Type of the target expression. |
source_location | Location to record in all created sub-expressions. |
ns | Namespace to perform type symbol/tag lookups. |
Definition at line 308 of file expr_initializer.cpp.