cprover
expr_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
24 class constant_exprt;
25 class exprt;
26 class symbol_exprt;
27 class update_exprt;
28 class with_exprt;
29 class if_exprt;
30 class symbolt;
31 class typet;
32 class namespacet;
33 
35 bool is_lvalue(const exprt &expr);
36 
38 exprt make_binary(const exprt &);
39 
42 
44 exprt is_not_zero(const exprt &, const namespacet &ns);
45 
48 exprt boolean_negate(const exprt &);
49 
51 bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
52 
54 bool has_subexpr(const exprt &, const irep_idt &);
55 
67 bool has_subtype(
68  const typet &type,
69  const std::function<bool(const typet &)> &pred,
70  const namespacet &ns);
71 
73 bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
74 
76 if_exprt lift_if(const exprt &, std::size_t operand_number);
77 
79 const exprt &skip_typecast(const exprt &expr);
80 
87 {
88 public:
90  bool operator()(const exprt &e) const
91  {
92  return is_constant(e);
93  }
94 
95 protected:
96  virtual bool is_constant(const exprt &) const;
97  virtual bool is_constant_address_of(const exprt &) const;
98 };
99 
102 
106 exprt make_and(exprt a, exprt b);
107 
108 #endif // CPROVER_UTIL_EXPR_UTIL_H
is_constantt
Determine whether an expression is constant.
Definition: expr_util.h:87
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
make_and
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
typet
The type of an expression, extends irept.
Definition: type.h:29
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
has_subtype
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:153
is_constantt::is_constant_address_of
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:254
exprt
Base class for all expressions.
Definition: expr.h:53
has_subexpr
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:139
lift_if
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:201
make_with_expr
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:67
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
make_boolean_expr
constant_exprt make_boolean_expr(bool)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
is_not_zero
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
boolean_negate
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
is_constantt::is_constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:227
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:23
is_constantt::operator()
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
Definition: expr_util.h:90
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3234
symbolt
Symbol table entry.
Definition: symbol.h:28
make_binary
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
irep.h