cprover
Loading...
Searching...
No Matches
simplify_expr_pointer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
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(is_null_pointer(constant))
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.base_type() = new_index_expr.type();
99
100 typecast_exprt typecast_expr(
101 from_integer((*step_size) * (*index) + address, c_index_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.base_type() = new_member_expr.type();
144 typecast_exprt typecast_expr(
145 from_integer(address + *offset, c_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.pointer();
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_base_type =
352 to_pointer_type(ptr_expr.front().type()).base_type();
353 if(pointer_base_type.id() == ID_empty)
354 pointer_base_type = char_type();
355
356 auto element_size = pointer_offset_size(pointer_base_type, ns);
357
358 if(!element_size.has_value())
359 return unchanged(expr);
360
361 exprt pointer_offset_expr = simplify_pointer_offset(
362 pointer_offset_exprt(ptr_expr.front(), expr.type()));
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.is_constant())
380 {
381 const constant_exprt &c_ptr = to_constant_expr(ptr);
382
383 if(is_null_pointer(c_ptr))
384 {
385 return from_integer(0, expr.type());
386 }
387 else
388 {
389 // this is a pointer, we can't use to_integer
390 const auto width = to_pointer_type(ptr.type()).get_width();
391 mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
392 // a null pointer would have been caught above, return value 0
393 // will indicate that conversion failed
394 if(number==0)
395 return unchanged(expr);
396
397 // The constant address consists of OBJECT-ID || OFFSET.
398 mp_integer offset_bits =
400 number%=power(2, offset_bits);
401
402 return from_integer(number, expr.type());
403 }
404 }
405
406 return unchanged(expr);
407}
408
410 const binary_relation_exprt &expr)
411{
412 // the operands of the relation are both either one of
413 // a) an address_of_exprt
414 // b) a typecast_exprt with an address_of_exprt operand
415
416 PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
417
418 // skip over the typecast
419 exprt tmp0 = skip_typecast(expr.op0());
420 PRECONDITION(tmp0.id() == ID_address_of);
421
422 auto &tmp0_address_of = to_address_of_expr(tmp0);
423
424 if(
425 tmp0_address_of.object().id() == ID_index &&
426 to_index_expr(tmp0_address_of.object()).index().is_zero())
427 {
428 tmp0_address_of =
429 address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
430 }
431
432 // skip over the typecast
433 exprt tmp1 = skip_typecast(expr.op1());
434 PRECONDITION(tmp1.id() == ID_address_of);
435
436 auto &tmp1_address_of = to_address_of_expr(tmp1);
437
438 if(
439 tmp1_address_of.object().id() == ID_index &&
440 to_index_expr(tmp1_address_of.object()).index().is_zero())
441 {
442 tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
443 }
444
445 const auto &tmp0_object = tmp0_address_of.object();
446 const auto &tmp1_object = tmp1_address_of.object();
447
448 if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
449 {
450 bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
451 to_symbol_expr(tmp1_object).get_identifier();
452
453 return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
454 }
455 else if(
456 tmp0_object.id() == ID_dynamic_object &&
457 tmp1_object.id() == ID_dynamic_object)
458 {
459 bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
461
462 return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
463 }
464 else if(
465 (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
466 (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
467 {
468 return make_boolean_expr(expr.id() != ID_equal);
469 }
470 else if(
471 tmp0_object.id() == ID_string_constant &&
472 tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
473 {
474 return make_boolean_expr(expr.id() == ID_equal);
475 }
476
477 return unchanged(expr);
478}
479
481 const binary_relation_exprt &expr)
482{
483 PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
484 PRECONDITION(expr.is_boolean());
485
486 exprt::operandst new_inequality_ops;
487 for(const auto &operand : expr.operands())
488 {
489 PRECONDITION(operand.id() == ID_pointer_object);
490 const exprt &op = to_pointer_object_expr(operand).pointer();
491
492 if(op.id()==ID_address_of)
493 {
494 const auto &op_object = to_address_of_expr(op).object();
495
496 if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
497 op_object.id() != ID_string_constant))
498 {
499 return unchanged(expr);
500 }
501 }
502 else if(!op.is_constant() || !op.is_zero())
503 {
504 return unchanged(expr);
505 }
506
507 if(new_inequality_ops.empty())
508 new_inequality_ops.push_back(op);
509 else
510 {
511 new_inequality_ops.push_back(
513 op, new_inequality_ops.front().type())));
514 }
515 }
516
517 auto new_expr = expr;
518
519 new_expr.operands() = std::move(new_inequality_ops);
520
521 return changed(simplify_inequality(new_expr));
522}
523
526{
527 const exprt &op = expr.pointer();
528
529 auto op_result = simplify_object(op);
530
531 if(op_result.expr.id() == ID_if)
532 {
533 const if_exprt &if_expr = to_if_expr(op_result.expr);
534 exprt cond=if_expr.cond();
535
536 auto p_o_false = expr;
537 p_o_false.op() = if_expr.false_case();
538
539 auto p_o_true = expr;
540 p_o_true.op() = if_expr.true_case();
541
542 auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
543 return changed(simplify_rec(new_expr));
544 }
545
546 if(op_result.has_changed())
547 {
548 auto new_expr = expr;
549 new_expr.op() = op_result;
550 return std::move(new_expr);
551 }
552 else
553 return unchanged(expr);
554}
555
558{
559 auto new_expr = expr;
560 exprt &op = new_expr.op();
561
562 if(op.id()==ID_if && op.operands().size()==3)
563 {
564 if_exprt if_expr=lift_if(expr, 0);
565 if_expr.true_case() =
567 if_expr.false_case() =
569 return changed(simplify_if(if_expr));
570 }
571
572 bool no_change = true;
573
574 auto op_result = simplify_object(op);
575
576 if(op_result.has_changed())
577 {
578 op = op_result.expr;
579 no_change = false;
580 }
581
582 // NULL is not dynamic
584 return false_exprt();
585
586 // &something depends on the something
587 if(op.id() == ID_address_of)
588 {
589 const auto &op_object = to_address_of_expr(op).object();
590
591 if(op_object.id() == ID_symbol)
592 {
593 const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
594
595 // this is for the benefit of symex
596 return make_boolean_expr(
597 has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::"));
598 }
599 else if(op_object.id() == ID_string_constant)
600 {
601 return false_exprt();
602 }
603 else if(op_object.id() == ID_array)
604 {
605 return false_exprt();
606 }
607 }
608
609 if(no_change)
610 return unchanged(expr);
611 else
612 return std::move(new_expr);
613}
614
617{
618 auto new_expr = expr;
619 exprt &op = new_expr.op();
620 bool no_change = true;
621
622 auto op_result = simplify_object(op);
623
624 if(op_result.has_changed())
625 {
626 op = op_result.expr;
627 no_change = false;
628 }
629
630 // NULL is not invalid
632 {
633 return false_exprt();
634 }
635
636 // &anything is not invalid
637 if(op.id()==ID_address_of)
638 {
639 return false_exprt();
640 }
641
642 if(no_change)
643 return unchanged(expr);
644 else
645 return std::move(new_expr);
646}
647
650{
651 auto new_expr = expr;
652 bool no_change = true;
653 exprt &op = new_expr.pointer();
654 auto op_result = simplify_object(op);
655
656 if(op_result.has_changed())
657 {
658 op = op_result.expr;
659 no_change = false;
660 }
661
662 if(op.id() == ID_address_of)
663 {
664 const auto &op_object = to_address_of_expr(op).object();
665
666 if(op_object.id() == ID_symbol)
667 {
668 // just get the type
669 auto size_opt = size_of_expr(op_object.type(), ns);
670
671 if(size_opt.has_value())
672 {
673 const typet &expr_type = expr.type();
674 exprt size = size_opt.value();
675
676 if(size.type() != expr_type)
677 size = simplify_typecast(typecast_exprt(size, expr_type));
678
679 return size;
680 }
681 }
682 else if(op_object.id() == ID_string_constant)
683 {
684 typet type=expr.type();
685 return from_integer(
686 to_string_constant(op_object).get_value().size() + 1, type);
687 }
688 }
689
690 if(no_change)
691 return unchanged(expr);
692 else
693 return std::move(new_expr);
694}
695
697 const prophecy_r_or_w_ok_exprt &expr)
698{
699 exprt new_expr = simplify_rec(expr.lower(ns));
700 if(!new_expr.is_constant())
701 return unchanged(expr);
702 else
703 return std::move(new_expr);
704}
705
708{
709 exprt new_expr = simplify_rec(expr.lower(ns));
710 if(!new_expr.is_constant())
711 return unchanged(expr);
712 else
713 return std::move(new_expr);
714}
configt config
Definition config.cpp:25
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)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
bitvector_typet char_type()
Definition c_types.cpp:111
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
std::size_t get_width() const
Definition std_types.h:876
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition std_expr.h:2942
const irep_idt & get_value() const
Definition std_expr.h:2950
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
unsigned int get_instance() const
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
exprt & op1()
Definition expr.h:128
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3017
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
const irep_idt & id() const
Definition irep.h:396
irep_idt get_component_name() const
Definition std_expr.h:2816
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
Definition std_expr.h:947
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
exprt lower(const namespacet &ns) const
A base class for a predicate that indicates that an address range is ok to read or write or both.
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const namespacet & ns
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
static resultt changed(resultt<> result)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_rec(const exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_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_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_object_size(const object_size_exprt &)
const irep_idt & get_identifier() const
Definition std_expr.h:142
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
const exprt & op() const
Definition std_expr.h:326
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
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...
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, 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< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
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:18
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:986
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const string_constantt & to_string_constant(const exprt &expr)
std::size_t object_bits
Definition config.h:348