CBMC
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 "deprecate.h"
21#include "irep.h"
22
23#include <functional>
24
25class constant_exprt;
26class exprt;
27class update_exprt;
28class with_exprt;
29class if_exprt;
30class typet;
31class namespacet;
32
38bool is_assignable(const exprt &);
39
41exprt make_binary(const exprt &);
42
44exprt is_not_zero(const exprt &, const namespacet &ns);
45
49
51bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
52
54bool has_subexpr(const exprt &, const irep_idt &);
55
67bool has_subtype(
68 const typet &type,
69 const std::function<bool(const typet &)> &pred,
70 const namespacet &ns);
71
73bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
74
76if_exprt lift_if(const exprt &, std::size_t operand_number);
77
79const exprt &skip_typecast(const exprt &expr);
80
87{
88public:
90 {
91 }
92
94 bool operator()(const exprt &e) const
95 {
96 return is_constant(e);
97 }
98
99protected:
101
102 virtual bool is_constant(const exprt &) const;
103 virtual bool is_constant_address_of(const exprt &) const;
104};
105
108
112DEPRECATED(SINCE(2025, 6, 25, "use conjunction(exprt, exprt) instead"))
114
115#endif // CPROVER_UTIL_EXPR_UTIL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Determine whether an expression is constant.
Definition expr_util.h:87
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:94
const namespacet & ns
Definition expr_util.h:100
can_forward_propagatet(const namespacet &ns)
Definition expr_util.h:89
A constant literal expression.
Definition std_expr.h:3118
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:2502
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:2783
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
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
Definition expr_util.cpp:98
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
Definition expr_util.cpp:69
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
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