cprover
value_set_dereference.cpp File Reference

Symbolic Execution of ANSI-C. More...

+ 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 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 bool is_a_bv_type ( const typet type)
static

Definition at line 581 of file value_set_dereference.cpp.

◆ should_use_local_definition_for()

static bool should_use_local_definition_for ( const exprt expr)
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.