10 #ifndef CPROVER_UTIL_EXPR_UTIL_H
11 #define CPROVER_UTIL_EXPR_UTIL_H
44 DEPRECATED(
SINCE(2024, 9, 10,
"use update_exprt::make_with_expr() instead"))
73 const std::function<
bool(const
typet &)> &pred,
107 virtual bool is_constant_address_of(
const exprt &)
const;
121 DEPRECATED(
SINCE(2024, 9, 10,
"use constant_exprt::is_null_pointer() instead"))
Determine whether an expression is constant.
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
can_forward_propagatet(const namespacet &ns)
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
The trinary if-then-else operator.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
#define SINCE(year, month, day, msg)
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
constant_exprt make_boolean_expr(bool)
returns true_exprt if given true and false_exprt otherwise
bool has_subexpr(const exprt &, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool is_assignable(const exprt &)
Returns true iff the argument is one of the following:
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
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.