CBMC
|
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"
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 . 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... | |
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. 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.cpp.
Typecast the input to the output if this is a signed/unsigned bv.
Perform a reinterpret cast using byte_extract otherwise.
expr | the expression to be casted if necessary. |
out_type | the type to cast the expression to. |
Definition at line 354 of file expr_initializer.cpp.
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.