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 {
93 }
94
96 bool operator()(const exprt &e) const
97 {
98 return is_constant(e);
99 }
100
101protected:
103
104 virtual bool is_constant(const exprt &) const;
105 virtual bool is_constant_address_of(const exprt &) const;
106};
107
110
115
119bool is_null_pointer(const constant_exprt &expr);
120
121#endif // CPROVER_UTIL_EXPR_UTIL_H
Determine whether an expression is constant.
Definition expr_util.h:89
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
Definition expr_util.h:96
const namespacet & ns
Definition expr_util.h:102
can_forward_propagatet(const namespacet &ns)
Definition expr_util.h:91
A constant literal expression.
Definition std_expr.h:2987
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
The trinary if-then-else operator.
Definition std_expr.h:2370
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2655
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
Definition expr_util.cpp:69
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
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:
Definition expr_util.cpp:24
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