cprover
Loading...
Searching...
No Matches
expr_util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_EXPR_UTIL_H
11#define CPROVER_UTIL_EXPR_UTIL_H
12
20#include "irep.h"
21
22#include <functional>
23
24class constant_exprt;
25class exprt;
26class update_exprt;
27class with_exprt;
28class if_exprt;
29class typet;
30class namespacet;
31
37bool is_assignable(const exprt &);
38
40exprt make_binary(const exprt &);
41
44
46exprt is_not_zero(const exprt &, const namespacet &ns);
47
51
53bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
54
56bool has_subexpr(const exprt &, const irep_idt &);
57
69bool has_subtype(
70 const typet &type,
71 const std::function<bool(const typet &)> &pred,
72 const namespacet &ns);
73
75bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
76
78if_exprt lift_if(const exprt &, std::size_t operand_number);
79
81const exprt &skip_typecast(const exprt &expr);
82
89{
90public:
92 bool operator()(const exprt &e) const
93 {
94 return is_constant(e);
95 }
96
97protected:
98 virtual bool is_constant(const exprt &) const;
99 virtual bool is_constant_address_of(const exprt &) const;
100};
101
104
109
110#endif // CPROVER_UTIL_EXPR_UTIL_H
A constant literal expression.
Definition: std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2226
Determine whether an expression is constant.
Definition: expr_util.h:89
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
Definition: expr_util.h:92
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:254
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:29
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:66
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
constant_exprt make_boolean_expr(bool)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
bool has_subexpr(const exprt &, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:200
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:97
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
bool is_assignable(const exprt &)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
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
Definition: expr_util.cpp:152