Symbolic Execution of ANSI-C. More...
#include "value_set_dereference.h"#include <util/arith_tools.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_expr.h>#include <util/fresh_symbol.h>#include <util/json.h>#include <util/message.h>#include <util/namespace.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.h>#include "dereference_callback.h"#include <deque>Go to the source code of this file.
expr is complicated enough that a local definition (using a let expression) is preferable to repeating it, potentially many times. 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 std::optional. Symbolic Execution of ANSI-C.
Definition in file value_set_dereference.cpp.
Definition at line 690 of file value_set_dereference.cpp.
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 51 of file value_set_dereference.cpp.
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 std::optional.
Definition at line 108 of file value_set_dereference.cpp.