cprover
expr_util.cpp File Reference
#include "expr_util.h"
#include <unordered_set>
#include "expr.h"
#include "expr_iterator.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "std_expr.h"
#include "symbol.h"
#include "namespace.h"
#include "arith_tools.h"
Include dependency graph for expr_util.cpp:

Go to the source code of this file.

Functions

bool is_lvalue (const exprt &expr)
 Returns true iff the argument is (syntactically) an lvalue. More...
 
exprt make_binary (const exprt &expr)
 splits an expression with >=3 operands into nested binary expressions More...
 
with_exprt make_with_expr (const update_exprt &src)
 converts an update expr into a (possibly nested) with expression More...
 
exprt is_not_zero (const exprt &src, const namespacet &ns)
 converts a scalar/float expression to C/C++ Booleans More...
 
exprt boolean_negate (const exprt &src)
 negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More...
 
bool has_subexpr (const exprt &expr, const std::function< bool(const exprt &)> &pred)
 returns true if the expression has a subexpression that satisfies pred More...
 
bool has_subexpr (const exprt &src, const irep_idt &id)
 returns true if the expression has a subexpression with given ID More...
 
bool has_subtype (const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
 returns true if any of the contained types satisfies pred More...
 
bool has_subtype (const typet &type, const irep_idt &id, const namespacet &ns)
 returns true if any of the contained types is id More...
 
if_exprt lift_if (const exprt &src, std::size_t operand_number)
 lift up an if_exprt one level More...
 
const exprtskip_typecast (const exprt &expr)
 find the expression nested inside typecasts, if any More...
 

Function Documentation

◆ boolean_negate()

◆ has_subexpr() [1/2]

bool has_subexpr ( const exprt expr,
const std::function< bool(const exprt &)> &  pred 
)

returns true if the expression has a subexpression that satisfies pred

Definition at line 138 of file expr_util.cpp.

References exprt::depth_begin(), and exprt::depth_end().

Referenced by goto_program_dereferencet::dereference_rec(), rw_range_set_value_sett::get_objects_dereference(), has_char_array_subexpr(), has_subexpr(), and goto_checkt::invalidate().

◆ has_subexpr() [2/2]

bool has_subexpr ( const exprt src,
const irep_idt id 
)

returns true if the expression has a subexpression with given ID

Definition at line 146 of file expr_util.cpp.

References has_subexpr(), and irept::id().

◆ has_subtype() [1/2]

bool has_subtype ( const typet type,
const std::function< bool(const typet &)> &  pred,
const namespacet ns 
)

returns true if any of the contained types satisfies pred

Parameters
typea type
preda predicate
nsnamespace for symbol type lookups
Returns
true if one of the subtype of type satisfies predicate pred. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... For instance in the type t defined by { int a; char[] b; double * c; { bool d} e}, int, char, double and bool are subtypes of t.

Definition at line 152 of file expr_util.cpp.

References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), stack, typet::subtypes(), to_c_enum_tag_type(), and to_struct_union_type().

Referenced by add_string_equation_to_symbol_resolution(), has_char_pointer_subtype(), has_subtype(), and string_identifiers_resolution_from_equations().

◆ has_subtype() [2/2]

bool has_subtype ( const typet type,
const irep_idt id,
const namespacet ns 
)

returns true if any of the contained types is id

Definition at line 192 of file expr_util.cpp.

References has_subtype(), and irept::id().

◆ is_lvalue()

bool is_lvalue ( const exprt expr)

Returns true iff the argument is (syntactically) an lvalue.

Definition at line 22 of file expr_util.cpp.

References index_exprt::array(), member_exprt::compound(), irept::id(), is_lvalue(), to_index_expr(), and to_member_expr().

Referenced by goto_convertt::do_function_call_symbol(), is_lvalue(), and make_va_list().

◆ is_not_zero()

◆ lift_if()

◆ make_binary()

exprt make_binary ( const exprt expr)

◆ make_with_expr()

with_exprt make_with_expr ( const update_exprt src)

converts an update expr into a (possibly nested) with expression

Definition at line 66 of file expr_util.cpp.

References update_exprt::designator(), forall_expr, index_designatort::index(), with_exprt::new_value(), PRECONDITION, to_index_designator(), to_with_expr(), UNREACHABLE, and with_exprt::where().

◆ skip_typecast()

const exprt& skip_typecast ( const exprt expr)