#include "value_set_dereference.h"#include <util/arith_tools.h>#include <util/byte_operators.h>#include <util/config.h>#include <util/cprover_prefix.h>#include <util/expr_iterator.h>#include <util/expr_util.h>#include <util/format_expr.h>#include <util/fresh_symbol.h>#include <util/json.h>#include <util/message.h>#include <util/pointer_expr.h>#include <util/pointer_offset_size.h>#include <util/pointer_predicates.h>#include <util/range.h>#include <util/simplify_expr.h>#include <util/symbol_table.h>#include <deque>#include "dereference_callback.h"
Include dependency graph for value_set_dereference.cpp:Go to the source code of this file.
Functions | |
| static bool | should_use_local_definition_for (const exprt &expr) |
Returns true if expr is complicated enough that a local definition (using a let expression) is preferable to repeating it, potentially many times. More... | |
| static json_objectt | value_set_dereference_stats_to_json (const exprt &pointer, const std::vector< exprt > &points_to_set, const std::vector< exprt > &retained_values, const exprt &value) |
| static optionalt< exprt > | try_add_offset_to_indices (const exprt &expr, const exprt &offset_elements) |
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ... otherwise return an empty optionalt. More... | |
| static bool | is_a_bv_type (const typet &type) |
Detailed Description
Symbolic Execution of ANSI-C
Definition in file value_set_dereference.cpp.
Function Documentation
◆ is_a_bv_type()
|
static |
Definition at line 665 of file value_set_dereference.cpp.
◆ should_use_local_definition_for()
|
static |
Returns true if expr is complicated enough that a local definition (using a let expression) is preferable to repeating it, potentially many times.
Of course this is just a heuristic – currently we allow any expression that only involves one symbol, such as "x", "(type*)x", "x[0]" (but not "x[y]"). Particularly we want to make sure to insist on a local definition of expr is a large if-expression, such as p == &o1 ? o1 : p == &o2 ? o2 : ..., as can result from dereferencing a subexpression (though note that value_set_dereferencet::dereference special-cases if_exprt, and therefore handles the specific case of a double-dereference (**p) without an intervening member operator, typecast, pointer arithmetic, etc.)
Definition at line 49 of file value_set_dereference.cpp.
◆ try_add_offset_to_indices()
|
static |
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ... otherwise return an empty optionalt.
Definition at line 106 of file value_set_dereference.cpp.
◆ value_set_dereference_stats_to_json()
|
static |
Definition at line 66 of file value_set_dereference.cpp.
