cprover
|
Symbolic Execution of ANSI-C. More...
#include "value_set_dereference.h"
#include <util/arith_tools.h>
#include <util/array_name.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/format_type.h>
#include <util/fresh_symbol.h>
#include <util/options.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <util/ssa_expr.h>
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 bool | is_a_bv_type (const typet &type) |
Symbolic Execution of ANSI-C.
Definition in file value_set_dereference.cpp.
|
static |
Definition at line 581 of file value_set_dereference.cpp.
|
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 46 of file value_set_dereference.cpp.