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
44DEPRECATED(SINCE(2024, 9, 10, "use update_exprt::make_with_expr() instead"))
46
49
53
55bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
56
59
71bool has_subtype(
72 const typet &type,
73 const std::function<bool(const typet &)> &pred,
74 const namespacet &ns);
75
78
81
84
91{
92public:
93 explicit can_forward_propagatet(const namespacet &ns) : ns(ns)
94 {
95 }
96
98 bool operator()(const exprt &e) const
99 {
100 return is_constant(e);
101 }
102
103protected:
105
106 virtual bool is_constant(const exprt &) const;
107 virtual bool is_constant_address_of(const exprt &) const;
108};
109
112
117
121DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead"))
123
124#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:91
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
Definition expr_util.h:98
const namespacet & ns
Definition expr_util.h:104
can_forward_propagatet(const namespacet &ns)
Definition expr_util.h:93
A constant literal expression.
Definition std_expr.h:3117
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:2497
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:2782
Operator to update elements in structs and arrays.
Definition std_expr.h:2598
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
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
Definition expr_util.cpp:74
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
STL namespace.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29