cprover
simplify_expr_pointer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
10 
11 #include "arith_tools.h"
12 #include "c_types.h"
13 #include "config.h"
14 #include "expr_util.h"
15 #include "namespace.h"
16 #include "pointer_expr.h"
17 #include "pointer_offset_size.h"
18 #include "pointer_predicates.h"
19 #include "prefix.h"
20 #include "std_expr.h"
21 #include "string_constant.h"
22 
24  const exprt &expr,
25  mp_integer &address)
26 {
27  if(expr.id() == ID_dereference)
28  {
29  const auto &pointer = to_dereference_expr(expr).pointer();
30 
31  if(
32  pointer.id() == ID_typecast &&
33  to_typecast_expr(pointer).op().is_constant() &&
34  !to_integer(to_constant_expr(to_typecast_expr(pointer).op()), address))
35  {
36  return true;
37  }
38 
39  if(pointer.is_constant())
40  {
41  const constant_exprt &constant = to_constant_expr(pointer);
42 
43  if(constant.get_value() == ID_NULL && config.ansi_c.NULL_is_zero) // NULL
44  {
45  address=0;
46  return true;
47  }
48  else if(!to_integer(constant, address))
49  return true;
50  }
51  }
52 
53  return false;
54 }
55 
58 {
59  if(expr.id()==ID_index)
60  {
61  auto new_index_expr = to_index_expr(expr);
62 
63  bool no_change = true;
64 
65  auto array_result = simplify_address_of_arg(new_index_expr.array());
66 
67  if(array_result.has_changed())
68  {
69  no_change = false;
70  new_index_expr.array() = array_result.expr;
71  }
72 
73  auto index_result = simplify_rec(new_index_expr.index());
74 
75  if(index_result.has_changed())
76  {
77  no_change = false;
78  new_index_expr.index() = index_result.expr;
79  }
80 
81  // rewrite (*(type *)int) [index] by
82  // pushing the index inside
83 
84  mp_integer address;
85  if(is_dereference_integer_object(new_index_expr.array(), address))
86  {
87  // push index into address
88  auto step_size = pointer_offset_size(new_index_expr.type(), ns);
89 
90  if(step_size.has_value())
91  {
92  const auto index = numeric_cast<mp_integer>(new_index_expr.index());
93 
94  if(index.has_value())
95  {
97  to_dereference_expr(new_index_expr.array()).pointer().type());
98  pointer_type.subtype() = new_index_expr.type();
99 
100  typecast_exprt typecast_expr(
101  from_integer((*step_size) * (*index) + address, index_type()),
102  pointer_type);
103 
104  return dereference_exprt{typecast_expr};
105  }
106  }
107  }
108 
109  if(!no_change)
110  return new_index_expr;
111  }
112  else if(expr.id()==ID_member)
113  {
114  auto new_member_expr = to_member_expr(expr);
115 
116  bool no_change = true;
117 
118  auto struct_op_result =
119  simplify_address_of_arg(new_member_expr.struct_op());
120 
121  if(struct_op_result.has_changed())
122  {
123  new_member_expr.struct_op() = struct_op_result.expr;
124  no_change = false;
125  }
126 
127  const typet &op_type = ns.follow(new_member_expr.struct_op().type());
128 
129  if(op_type.id() == ID_struct)
130  {
131  // rewrite NULL -> member by
132  // pushing the member inside
133 
134  mp_integer address;
135  if(is_dereference_integer_object(new_member_expr.struct_op(), address))
136  {
137  const irep_idt &member = to_member_expr(expr).get_component_name();
138  auto offset = member_offset(to_struct_type(op_type), member, ns);
139  if(offset.has_value())
140  {
142  to_dereference_expr(new_member_expr.struct_op()).pointer().type());
143  pointer_type.subtype() = new_member_expr.type();
144  typecast_exprt typecast_expr(
145  from_integer(address + *offset, index_type()), pointer_type);
146  return dereference_exprt{typecast_expr};
147  }
148  }
149  }
150 
151  if(!no_change)
152  return new_member_expr;
153  }
154  else if(expr.id()==ID_dereference)
155  {
156  auto new_expr = to_dereference_expr(expr);
157  auto r_pointer = simplify_rec(new_expr.pointer());
158  if(r_pointer.has_changed())
159  {
160  new_expr.pointer() = r_pointer.expr;
161  return std::move(new_expr);
162  }
163  }
164  else if(expr.id()==ID_if)
165  {
166  auto new_if_expr = to_if_expr(expr);
167 
168  bool no_change = true;
169 
170  auto r_cond = simplify_rec(new_if_expr.cond());
171  if(r_cond.has_changed())
172  {
173  new_if_expr.cond() = r_cond.expr;
174  no_change = false;
175  }
176 
177  auto true_result = simplify_address_of_arg(new_if_expr.true_case());
178  if(true_result.has_changed())
179  {
180  new_if_expr.true_case() = true_result.expr;
181  no_change = false;
182  }
183 
184  auto false_result = simplify_address_of_arg(new_if_expr.false_case());
185 
186  if(false_result.has_changed())
187  {
188  new_if_expr.false_case() = false_result.expr;
189  no_change = false;
190  }
191 
192  // condition is a constant?
193  if(new_if_expr.cond().is_true())
194  {
195  return new_if_expr.true_case();
196  }
197  else if(new_if_expr.cond().is_false())
198  {
199  return new_if_expr.false_case();
200  }
201 
202  if(!no_change)
203  return new_if_expr;
204  }
205 
206  return unchanged(expr);
207 }
208 
211 {
212  if(expr.type().id() != ID_pointer)
213  return unchanged(expr);
214 
215  auto new_object = simplify_address_of_arg(expr.object());
216 
217  if(new_object.expr.id() == ID_index)
218  {
219  auto index_expr = to_index_expr(new_object.expr);
220 
221  if(!index_expr.index().is_zero())
222  {
223  // we normalize &a[i] to (&a[0])+i
224  exprt offset = index_expr.op1();
225  index_expr.op1()=from_integer(0, offset.type());
226  auto new_address_of_expr = expr;
227  new_address_of_expr.object() = std::move(index_expr);
228  return plus_exprt(std::move(new_address_of_expr), offset);
229  }
230  }
231  else if(new_object.expr.id() == ID_dereference)
232  {
233  // simplify &*p to p
234  return to_dereference_expr(new_object.expr).pointer();
235  }
236 
237  if(new_object.has_changed())
238  {
239  auto new_expr = expr;
240  new_expr.object() = new_object;
241  return new_expr;
242  }
243  else
244  return unchanged(expr);
245 }
246 
249 {
250  const exprt &ptr = expr.op();
251 
252  if(ptr.id()==ID_if && ptr.operands().size()==3)
253  {
254  if_exprt if_expr=lift_if(expr, 0);
255  if_expr.true_case() =
257  if_expr.false_case() =
259  return changed(simplify_if(if_expr));
260  }
261 
262  if(ptr.type().id()!=ID_pointer)
263  return unchanged(expr);
264 
265  if(ptr.id()==ID_address_of)
266  {
267  auto offset = compute_pointer_offset(to_address_of_expr(ptr).object(), ns);
268 
269  if(offset.has_value())
270  return from_integer(*offset, expr.type());
271  }
272  else if(ptr.id()==ID_typecast) // pointer typecast
273  {
274  const auto &op = to_typecast_expr(ptr).op();
275  const typet &op_type = op.type();
276 
277  if(op_type.id()==ID_pointer)
278  {
279  // Cast from pointer to pointer.
280  // This just passes through, remove typecast.
281  auto new_expr = expr;
282  new_expr.op() = op;
283 
284  return changed(simplify_pointer_offset(new_expr)); // recursive call
285  }
286  else if(op_type.id()==ID_signedbv ||
287  op_type.id()==ID_unsignedbv)
288  {
289  // Cast from integer to pointer, say (int *)x.
290 
291  if(op.is_constant())
292  {
293  // (T *)0x1234 -> 0x1234
294  return changed(simplify_typecast(typecast_exprt{op, expr.type()}));
295  }
296  else
297  {
298  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
299  // which is re-written to 'a'.
300 
301  typet type = expr.type();
302  exprt tmp = op;
303  if(tmp.id()==ID_plus && tmp.operands().size()==2)
304  {
305  const auto &plus_expr = to_plus_expr(tmp);
306 
307  if(
308  plus_expr.op0().id() == ID_typecast &&
309  to_typecast_expr(plus_expr.op0()).op().id() == ID_address_of)
310  {
311  auto new_expr =
312  typecast_exprt::conditional_cast(plus_expr.op1(), type);
313 
314  return changed(simplify_node(new_expr));
315  }
316  else if(
317  plus_expr.op1().id() == ID_typecast &&
318  to_typecast_expr(plus_expr.op1()).op().id() == ID_address_of)
319  {
320  auto new_expr =
321  typecast_exprt::conditional_cast(plus_expr.op0(), type);
322 
323  return changed(simplify_node(new_expr));
324  }
325  }
326  }
327  }
328  }
329  else if(ptr.id()==ID_plus) // pointer arithmetic
330  {
331  exprt::operandst ptr_expr;
332  exprt::operandst int_expr;
333 
334  for(const auto &op : ptr.operands())
335  {
336  if(op.type().id()==ID_pointer)
337  ptr_expr.push_back(op);
338  else if(!op.is_zero())
339  {
340  exprt tmp=op;
341  if(tmp.type()!=expr.type())
342  tmp = simplify_typecast(typecast_exprt(tmp, expr.type()));
343 
344  int_expr.push_back(tmp);
345  }
346  }
347 
348  if(ptr_expr.size()!=1 || int_expr.empty())
349  return unchanged(expr);
350 
351  typet pointer_sub_type=ptr_expr.front().type().subtype();
352  if(pointer_sub_type.id()==ID_empty)
353  pointer_sub_type=char_type();
354 
355  auto element_size = pointer_offset_size(pointer_sub_type, ns);
356 
357  if(!element_size.has_value())
358  return unchanged(expr);
359 
360  // this might change the type of the pointer!
361  exprt pointer_offset_expr =
363 
364  exprt sum;
365 
366  if(int_expr.size()==1)
367  sum=int_expr.front();
368  else
369  sum = simplify_plus(plus_exprt{int_expr, expr.type()});
370 
371  exprt size_expr = from_integer(*element_size, expr.type());
372 
373  exprt product = simplify_mult(mult_exprt{sum, size_expr});
374 
375  auto new_expr = plus_exprt(pointer_offset_expr, product);
376 
377  return changed(simplify_plus(new_expr));
378  }
379  else if(ptr.id()==ID_constant)
380  {
381  const constant_exprt &c_ptr = to_constant_expr(ptr);
382 
383  if(c_ptr.get_value()==ID_NULL ||
384  c_ptr.value_is_zero_string())
385  {
386  return from_integer(0, expr.type());
387  }
388  else
389  {
390  // this is a pointer, we can't use to_integer
391  const auto width = to_pointer_type(ptr.type()).get_width();
392  mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
393  // a null pointer would have been caught above, return value 0
394  // will indicate that conversion failed
395  if(number==0)
396  return unchanged(expr);
397 
398  // The constant address consists of OBJECT-ID || OFFSET.
399  mp_integer offset_bits =
401  number%=power(2, offset_bits);
402 
403  return from_integer(number, expr.type());
404  }
405  }
406 
407  return unchanged(expr);
408 }
409 
411  const binary_relation_exprt &expr)
412 {
413  // the operands of the relation are both either one of
414  // a) an address_of_exprt
415  // b) a typecast_exprt with an address_of_exprt operand
416 
417  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
418 
419  // skip over the typecast
420  exprt tmp0 = skip_typecast(expr.op0());
421  PRECONDITION(tmp0.id() == ID_address_of);
422 
423  auto &tmp0_address_of = to_address_of_expr(tmp0);
424 
425  if(
426  tmp0_address_of.object().id() == ID_index &&
427  to_index_expr(tmp0_address_of.object()).index().is_zero())
428  {
429  tmp0_address_of =
430  address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
431  }
432 
433  // skip over the typecast
434  exprt tmp1 = skip_typecast(expr.op1());
435  PRECONDITION(tmp1.id() == ID_address_of);
436 
437  auto &tmp1_address_of = to_address_of_expr(tmp1);
438 
439  if(
440  tmp1_address_of.object().id() == ID_index &&
441  to_index_expr(tmp1_address_of.object()).index().is_zero())
442  {
443  tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
444  }
445 
446  const auto &tmp0_object = tmp0_address_of.object();
447  const auto &tmp1_object = tmp1_address_of.object();
448 
449  if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
450  {
451  bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
452  to_symbol_expr(tmp1_object).get_identifier();
453 
454  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
455  }
456  else if(
457  tmp0_object.id() == ID_dynamic_object &&
458  tmp1_object.id() == ID_dynamic_object)
459  {
460  bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
461  to_dynamic_object_expr(tmp1_object).get_instance();
462 
463  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
464  }
465  else if(
466  (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
467  (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
468  {
469  return make_boolean_expr(expr.id() != ID_equal);
470  }
471 
472  return unchanged(expr);
473 }
474 
476  const binary_relation_exprt &expr)
477 {
478  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
479  PRECONDITION(expr.type().id() == ID_bool);
480 
481  exprt::operandst new_inequality_ops;
482  forall_operands(it, expr)
483  {
484  PRECONDITION(it->id() == ID_pointer_object);
485  const exprt &op = to_unary_expr(*it).op();
486 
487  if(op.id()==ID_address_of)
488  {
489  const auto &op_object = to_address_of_expr(op).object();
490 
491  if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
492  op_object.id() != ID_string_constant))
493  {
494  return unchanged(expr);
495  }
496  }
497  else if(op.id() != ID_constant || !op.is_zero())
498  {
499  return unchanged(expr);
500  }
501 
502  if(new_inequality_ops.empty())
503  new_inequality_ops.push_back(op);
504  else
505  {
506  new_inequality_ops.push_back(
508  op, new_inequality_ops.front().type())));
509  }
510  }
511 
512  auto new_expr = expr;
513 
514  new_expr.operands() = std::move(new_inequality_ops);
515 
516  return changed(simplify_inequality(new_expr));
517 }
518 
521 {
522  const exprt &op = expr.op();
523 
524  auto op_result = simplify_object(op);
525 
526  if(op_result.expr.id() == ID_if)
527  {
528  const if_exprt &if_expr = to_if_expr(op_result.expr);
529  exprt cond=if_expr.cond();
530 
531  auto p_o_false = expr;
532  p_o_false.op() = if_expr.false_case();
533 
534  auto p_o_true = expr;
535  p_o_true.op() = if_expr.true_case();
536 
537  auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
538  return changed(simplify_rec(new_expr));
539  }
540 
541  if(op_result.has_changed())
542  {
543  auto new_expr = expr;
544  new_expr.op() = op_result;
545  return std::move(new_expr);
546  }
547  else
548  return unchanged(expr);
549 }
550 
553 {
554  auto new_expr = expr;
555  exprt &op = new_expr.op();
556 
557  if(op.id()==ID_if && op.operands().size()==3)
558  {
559  if_exprt if_expr=lift_if(expr, 0);
560  if_expr.true_case() =
562  if_expr.false_case() =
564  return changed(simplify_if(if_expr));
565  }
566 
567  bool no_change = true;
568 
569  auto op_result = simplify_object(op);
570 
571  if(op_result.has_changed())
572  {
573  op = op_result.expr;
574  no_change = false;
575  }
576 
577  // NULL is not dynamic
578  if(op.id() == ID_constant && op.get(ID_value) == ID_NULL)
579  return false_exprt();
580 
581  // &something depends on the something
582  if(op.id() == ID_address_of)
583  {
584  const auto &op_object = to_address_of_expr(op).object();
585 
586  if(op_object.id() == ID_symbol)
587  {
588  const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
589 
590  // this is for the benefit of symex
591  return make_boolean_expr(
593  }
594  else if(op_object.id() == ID_string_constant)
595  {
596  return false_exprt();
597  }
598  else if(op_object.id() == ID_array)
599  {
600  return false_exprt();
601  }
602  }
603 
604  if(no_change)
605  return unchanged(expr);
606  else
607  return std::move(new_expr);
608 }
609 
612 {
613  auto new_expr = expr;
614  exprt &op = new_expr.op();
615  bool no_change = true;
616 
617  auto op_result = simplify_object(op);
618 
619  if(op_result.has_changed())
620  {
621  op = op_result.expr;
622  no_change = false;
623  }
624 
625  // NULL is not invalid
626  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
627  {
628  return false_exprt();
629  }
630 
631  // &anything is not invalid
632  if(op.id()==ID_address_of)
633  {
634  return false_exprt();
635  }
636 
637  if(no_change)
638  return unchanged(expr);
639  else
640  return std::move(new_expr);
641 }
642 
645 {
646  auto new_expr = expr;
647  bool no_change = true;
648  exprt &op = new_expr.op();
649  auto op_result = simplify_object(op);
650 
651  if(op_result.has_changed())
652  {
653  op = op_result.expr;
654  no_change = false;
655  }
656 
657  if(op.id() == ID_address_of)
658  {
659  const auto &op_object = to_address_of_expr(op).object();
660 
661  if(op_object.id() == ID_symbol)
662  {
663  // just get the type
664  auto size_opt = size_of_expr(op_object.type(), ns);
665 
666  if(size_opt.has_value())
667  {
668  const typet &expr_type = expr.type();
669  exprt size = size_opt.value();
670 
671  if(size.type() != expr_type)
672  size = simplify_typecast(typecast_exprt(size, expr_type));
673 
674  return size;
675  }
676  }
677  else if(op_object.id() == ID_string_constant)
678  {
679  typet type=expr.type();
680  return from_integer(
681  to_string_constant(op_object).get_value().size() + 1, type);
682  }
683  }
684 
685  if(no_change)
686  return unchanged(expr);
687  else
688  return std::move(new_expr);
689 }
690 
693 {
694  // we expand the definition
695  exprt def = good_pointer_def(expr.op(), ns);
696 
697  // recursive call
698  return changed(simplify_rec(def));
699 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
bitvector_typet index_type()
Definition: c_types.cpp:16
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bitvector_typet char_type()
Definition: c_types.cpp:114
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt & object()
Definition: pointer_expr.h:350
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:843
struct configt::bv_encodingt bv_encoding
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2753
const irep_idt & get_value() const
Definition: std_expr.h:2761
bool value_is_zero_string() const
Definition: std_expr.cpp:16
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
unsigned int get_instance() const
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt & op1()
Definition: expr.h:102
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
irep_idt get_component_name() const
Definition: std_expr.h:2627
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const namespacet & ns
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_good_pointer(const unary_exprt &)
static resultt changed(resultt<> result)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_address_of_arg(const exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_object_size(const unary_exprt &)
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_pointer_object(const unary_exprt &)
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define forall_operands(it, expr)
Definition: expr.h:18
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:281
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:281
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const string_constantt & to_string_constant(const exprt &expr)
bool NULL_is_zero
Definition: config.h:167
std::size_t object_bits
Definition: config.h:255