symex_clean_expr.cpp File Reference
#include "goto_symex.h"#include <util/arith_tools.h>#include <util/byte_operators.h>#include <util/c_types.h>#include <util/expr_iterator.h>#include <util/nodiscard.h>#include <util/pointer_offset_size.h>#include <util/simplify_expr.h>#include "expr_skeleton.h"#include "path_storage.h"#include "symex_assign.h"#include "symex_dereference_state.h"#include <pointer-analysis/value_set_dereference.h>
Include dependency graph for symex_clean_expr.cpp:Go to the source code of this file.
Functions | |
| static void | process_array_expr (exprt &expr, bool do_simplify, const namespacet &ns) |
| Given an expression, find the root object and the offset into it. More... | |
| static void | adjust_byte_extract_rec (exprt &expr, const namespacet &ns) |
| Rewrite index/member expressions in byte_extract to offset. More... | |
| static void | replace_nondet (exprt &expr, symex_nondet_generatort &build_symex_nondet) |
Detailed Description
Symbolic Execution of ANSI-C
Definition in file symex_clean_expr.cpp.
Function Documentation
◆ adjust_byte_extract_rec()
|
static |
Rewrite index/member expressions in byte_extract to offset.
Definition at line 144 of file symex_clean_expr.cpp.
◆ process_array_expr()
|
static |
Given an expression, find the root object and the offset into it.
The extra complication to be considered here is that the expression may have any number of ternary expressions mixed with type casts.
Definition at line 34 of file symex_clean_expr.cpp.
◆ replace_nondet()
|
static |
Definition at line 166 of file symex_clean_expr.cpp.
