cprover
|
#include "expr_util.h"
#include <algorithm>
#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"
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 exprt & | skip_typecast (const exprt &expr) |
find the expression nested inside typecasts, if any More... | |
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition at line 127 of file expr_util.cpp.
returns true if the expression has a subexpression that satisfies pred
Definition at line 139 of file expr_util.cpp.
returns true if the expression has a subexpression with given ID
Definition at line 147 of file expr_util.cpp.
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
type | a type |
pred | a predicate |
ns | namespace for symbol type lookups |
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 153 of file expr_util.cpp.
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 193 of file expr_util.cpp.
bool is_lvalue | ( | const exprt & | expr | ) |
Returns true iff the argument is (syntactically) an lvalue.
Definition at line 23 of file expr_util.cpp.
exprt is_not_zero | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
converts a scalar/float expression to C/C++ Booleans
Definition at line 98 of file expr_util.cpp.
lift up an if_exprt one level
Definition at line 199 of file expr_util.cpp.
splits an expression with >=3 operands into nested binary expressions
Definition at line 36 of file expr_util.cpp.
with_exprt make_with_expr | ( | const update_exprt & | src | ) |
converts an update expr into a (possibly nested) with expression
Definition at line 67 of file expr_util.cpp.
find the expression nested inside typecasts, if any
Definition at line 219 of file expr_util.cpp.