CBMC
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 "deprecate.h"
21 #include "irep.h"
22 
23 #include <functional>
24 
25 class constant_exprt;
26 class exprt;
27 class update_exprt;
28 class with_exprt;
29 class if_exprt;
30 class typet;
31 class namespacet;
32 
38 bool is_assignable(const exprt &);
39 
41 exprt make_binary(const exprt &);
42 
44 DEPRECATED(SINCE(2024, 9, 10, "use update_exprt::make_with_expr() instead"))
46 
48 exprt is_not_zero(const exprt &, const namespacet &ns);
49 
52 exprt boolean_negate(const exprt &);
53 
55 bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
56 
58 bool has_subexpr(const exprt &, const irep_idt &);
59 
71 bool has_subtype(
72  const typet &type,
73  const std::function<bool(const typet &)> &pred,
74  const namespacet &ns);
75 
77 bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
78 
80 if_exprt lift_if(const exprt &, std::size_t operand_number);
81 
83 const exprt &skip_typecast(const exprt &expr);
84 
91 {
92 public:
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 
103 protected:
104  const namespacet &ns;
105 
106  virtual bool is_constant(const exprt &) const;
107  virtual bool is_constant_address_of(const exprt &) const;
108 };
109 
112 
116 exprt make_and(exprt a, exprt b);
117 
121 DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead"))
122 bool is_null_pointer(const constant_exprt &expr);
123 
124 #endif // CPROVER_UTIL_EXPR_UTIL_H
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:2990
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
#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
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
constant_exprt make_boolean_expr(bool)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:313
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:115
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
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
Definition: expr_util.cpp:177
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.
Definition: expr_util.cpp:321
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...
Definition: expr_util.cpp:344
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
Definition: expr_util.cpp:129
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29