#include "expr_initializer.h"#include "arith_tools.h"#include "c_types.h"#include "magic.h"#include "namespace.h"#include "pointer_offset_size.h"#include "std_code.h"
Include dependency graph for expr_initializer.cpp:Go to the source code of this file.
Classes | |
| class | expr_initializert< nondet > |
Functions | |
| optionalt< exprt > | zero_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns) |
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.cpp.
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.
