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 <cassert>
12 
13 #include "arith_tools.h"
14 #include "c_types.h"
15 #include "config.h"
16 #include "expr_util.h"
17 #include "namespace.h"
18 #include "pointer_offset_size.h"
19 #include "pointer_predicates.h"
20 #include "std_expr.h"
21 #include "threeval.h"
22 
24  const exprt &expr,
25  mp_integer &address)
26 {
27  if(expr.id()==ID_dereference &&
28  expr.operands().size()==1)
29  {
30  if(expr.op0().id()==ID_typecast &&
31  expr.op0().operands().size()==1 &&
32  expr.op0().op0().is_constant() &&
33  !to_integer(expr.op0().op0(), address))
34  return true;
35 
36  if(expr.op0().is_constant())
37  {
38  if(to_constant_expr(expr.op0()).get_value()==ID_NULL &&
39  config.ansi_c.NULL_is_zero) // NULL
40  {
41  address=0;
42  return true;
43  }
44  else if(!to_integer(expr.op0(), address))
45  return true;
46  }
47  }
48 
49  return false;
50 }
51 
53 {
54  if(expr.id()==ID_index)
55  {
56  if(expr.operands().size()==2)
57  {
58  bool result=true;
59  if(!simplify_address_of_arg(expr.op0()))
60  result=false;
61  if(!simplify_rec(expr.op1()))
62  result=false;
63 
64  // rewrite (*(type *)int) [index] by
65  // pushing the index inside
66 
67  mp_integer address;
68  if(is_dereference_integer_object(expr.op0(), address))
69  {
70  // push index into address
71  auto step_size = pointer_offset_size(expr.type(), ns);
72 
73  if(step_size.has_value())
74  {
75  mp_integer index;
76 
77  if(!to_integer(expr.op1(), index))
78  {
81  pointer_type.subtype() = expr.type();
82 
83  typecast_exprt typecast_expr(
84  from_integer((*step_size) * index + address, index_type()),
85  pointer_type);
86 
87  expr = dereference_exprt(typecast_expr, expr.type());
88  result = true;
89  }
90  }
91  }
92 
93  return result;
94  }
95  }
96  else if(expr.id()==ID_member)
97  {
98  if(expr.operands().size()==1)
99  {
100  bool result=true;
101  if(!simplify_address_of_arg(expr.op0()))
102  result=false;
103 
104  const typet &op_type=ns.follow(expr.op0().type());
105 
106  if(op_type.id()==ID_struct)
107  {
108  // rewrite NULL -> member by
109  // pushing the member inside
110 
111  mp_integer address;
112  if(is_dereference_integer_object(expr.op0(), address))
113  {
114  const struct_typet &struct_type=to_struct_type(op_type);
115  const irep_idt &member=to_member_expr(expr).get_component_name();
116  auto offset = member_offset(struct_type, member, ns);
117  if(offset.has_value())
118  {
121  pointer_type.subtype()=expr.type();
122  typecast_exprt typecast_expr(
123  from_integer(address + *offset, index_type()), pointer_type);
124  expr = dereference_exprt(typecast_expr, expr.type());
125  result=true;
126  }
127  }
128  }
129 
130  return result;
131  }
132  }
133  else if(expr.id()==ID_dereference)
134  {
135  if(expr.operands().size()==1)
136  return simplify_rec(expr.op0());
137  }
138  else if(expr.id()==ID_if)
139  {
140  if(expr.operands().size()==3)
141  {
142  bool result=true;
143  if(!simplify_rec(expr.op0()))
144  result=false;
145  if(!simplify_address_of_arg(expr.op1()))
146  result=false;
147  if(!simplify_address_of_arg(expr.op2()))
148  result=false;
149 
150  // op0 is a constant?
151  if(expr.op0().is_true())
152  {
153  result=false;
154  exprt tmp;
155  tmp.swap(expr.op1());
156  expr.swap(tmp);
157  }
158  else if(expr.op0().is_false())
159  {
160  result=false;
161  exprt tmp;
162  tmp.swap(expr.op2());
163  expr.swap(tmp);
164  }
165 
166  return result;
167  }
168  }
169 
170  return true;
171 }
172 
174 {
175  if(expr.operands().size()!=1)
176  return true;
177 
178  if(ns.follow(expr.type()).id()!=ID_pointer)
179  return true;
180 
181  exprt &object=expr.op0();
182 
183  bool result=simplify_address_of_arg(object);
184 
185  if(object.id()==ID_index)
186  {
187  index_exprt &index_expr=to_index_expr(object);
188 
189  if(!index_expr.index().is_zero())
190  {
191  // we normalize &a[i] to (&a[0])+i
192  exprt offset;
193  offset.swap(index_expr.op1());
194  index_expr.op1()=from_integer(0, offset.type());
195 
196  expr = plus_exprt(expr, offset);
197  return false;
198  }
199  }
200  else if(object.id()==ID_dereference)
201  {
202  // simplify &*p to p
203  auto const &object_as_dereference_expr = to_dereference_expr(object);
204  expr = object_as_dereference_expr.pointer();
205  return false;
206  }
207 
208  return result;
209 }
210 
212 {
213  if(expr.operands().size()!=1)
214  return true;
215 
216  exprt &ptr=expr.op0();
217 
218  if(ptr.id()==ID_if && ptr.operands().size()==3)
219  {
220  if_exprt if_expr=lift_if(expr, 0);
223  simplify_if(if_expr);
224  expr.swap(if_expr);
225 
226  return false;
227  }
228 
229  if(ptr.type().id()!=ID_pointer)
230  return true;
231 
232  if(ptr.id()==ID_address_of)
233  {
234  if(ptr.operands().size()!=1)
235  return true;
236 
237  auto offset = compute_pointer_offset(ptr.op0(), ns);
238 
239  if(offset.has_value())
240  {
241  expr = from_integer(*offset, expr.type());
242  return false;
243  }
244  }
245  else if(ptr.id()==ID_typecast) // pointer typecast
246  {
247  if(ptr.operands().size()!=1)
248  return true;
249 
250  const typet &op_type=ns.follow(ptr.op0().type());
251 
252  if(op_type.id()==ID_pointer)
253  {
254  // Cast from pointer to pointer.
255  // This just passes through, remove typecast.
256  exprt tmp=ptr.op0();
257  ptr=tmp;
258 
259  // recursive call
260  simplify_node(expr);
261  return false;
262  }
263  else if(op_type.id()==ID_signedbv ||
264  op_type.id()==ID_unsignedbv)
265  {
266  // Cast from integer to pointer, say (int *)x.
267 
268  if(ptr.op0().is_constant())
269  {
270  // (T *)0x1234 -> 0x1234
271  exprt tmp=ptr.op0();
272  tmp.make_typecast(expr.type());
273  simplify_node(tmp);
274  expr.swap(tmp);
275  return false;
276  }
277  else
278  {
279  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
280  // which is re-written to 'a'.
281 
282  typet type=ns.follow(expr.type());
283  exprt tmp=ptr.op0();
284  if(tmp.id()==ID_plus && tmp.operands().size()==2)
285  {
286  if(tmp.op0().id()==ID_typecast &&
287  tmp.op0().operands().size()==1 &&
288  tmp.op0().op0().id()==ID_address_of)
289  {
290  expr=tmp.op1();
291  if(type!=expr.type())
292  expr.make_typecast(type);
293 
294  simplify_node(expr);
295  return false;
296  }
297  else if(tmp.op1().id()==ID_typecast &&
298  tmp.op1().operands().size()==1 &&
299  tmp.op1().op0().id()==ID_address_of)
300  {
301  expr=tmp.op0();
302  if(type!=expr.type())
303  expr.make_typecast(type);
304 
305  simplify_node(expr);
306  return false;
307  }
308  }
309  }
310  }
311  }
312  else if(ptr.id()==ID_plus) // pointer arithmetic
313  {
314  exprt::operandst ptr_expr;
315  exprt::operandst int_expr;
316 
317  for(const auto &op : ptr.operands())
318  {
319  if(op.type().id()==ID_pointer)
320  ptr_expr.push_back(op);
321  else if(!op.is_zero())
322  {
323  exprt tmp=op;
324  if(tmp.type()!=expr.type())
325  {
326  tmp.make_typecast(expr.type());
327  simplify_node(tmp);
328  }
329 
330  int_expr.push_back(tmp);
331  }
332  }
333 
334  if(ptr_expr.size()!=1 || int_expr.empty())
335  return true;
336 
337  typet pointer_sub_type=ptr_expr.front().type().subtype();
338  if(pointer_sub_type.id()==ID_empty)
339  pointer_sub_type=char_type();
340 
341  auto element_size = pointer_offset_size(pointer_sub_type, ns);
342 
343  if(!element_size.has_value())
344  return true;
345 
346  // this might change the type of the pointer!
347  exprt pointer_offset_expr=pointer_offset(ptr_expr.front());
348  simplify_node(pointer_offset_expr);
349 
350  exprt sum;
351 
352  if(int_expr.size()==1)
353  sum=int_expr.front();
354  else
355  {
356  sum=exprt(ID_plus, expr.type());
357  sum.operands()=int_expr;
358  }
359 
360  simplify_node(sum);
361 
362  exprt size_expr = from_integer(*element_size, expr.type());
363 
364  binary_exprt product(sum, ID_mult, size_expr, expr.type());
365 
366  simplify_node(product);
367 
368  expr=binary_exprt(pointer_offset_expr, ID_plus, product, expr.type());
369 
370  simplify_node(expr);
371 
372  return false;
373  }
374  else if(ptr.id()==ID_constant)
375  {
376  constant_exprt &c_ptr=to_constant_expr(ptr);
377 
378  if(c_ptr.get_value()==ID_NULL ||
379  c_ptr.value_is_zero_string())
380  {
381  expr=from_integer(0, expr.type());
382 
383  simplify_node(expr);
384 
385  return false;
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 true;
396 
397  // The constant address consists of OBJECT-ID || OFFSET.
398  mp_integer offset_bits =
400  number%=power(2, offset_bits);
401 
402  expr=from_integer(number, expr.type());
403 
404  simplify_node(expr);
405 
406  return false;
407  }
408  }
409 
410  return true;
411 }
412 
414 {
415  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
416  PRECONDITION(expr.type().id() == ID_bool);
418  expr.operands().size() == 2, "(in)equalities have two operands");
419 
420  exprt tmp0=expr.op0();
421  if(tmp0.id()==ID_typecast)
422  tmp0=expr.op0().op0();
423  if(tmp0.op0().id()==ID_index &&
424  to_index_expr(tmp0.op0()).index().is_zero())
425  tmp0=address_of_exprt(to_index_expr(tmp0.op0()).array());
426  exprt tmp1=expr.op1();
427  if(tmp1.id()==ID_typecast)
428  tmp1=expr.op1().op0();
429  if(tmp1.op0().id()==ID_index &&
430  to_index_expr(tmp1.op0()).index().is_zero())
431  tmp1=address_of_exprt(to_index_expr(tmp1.op0()).array());
432  INVARIANT(tmp0.id() == ID_address_of, "id must be ID_address_of");
433  INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of");
434 
435  if(tmp0.operands().size()!=1)
436  return true;
437  if(tmp1.operands().size()!=1)
438  return true;
439 
440  if(tmp0.op0().id()==ID_symbol &&
441  tmp1.op0().id()==ID_symbol)
442  {
443  bool equal = to_symbol_expr(tmp0.op0()).get_identifier() ==
445 
446  expr.make_bool(expr.id()==ID_equal?equal:!equal);
447 
448  return false;
449  }
450 
451  return true;
452 }
453 
455 {
456  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
457  PRECONDITION(expr.type().id() == ID_bool);
459  expr.operands().size() == 2, "(in)equalities have two operands");
460 
461  forall_operands(it, expr)
462  {
463  PRECONDITION(it->id() == ID_pointer_object);
464  PRECONDITION(it->operands().size() == 1);
465  const exprt &op=it->op0();
466 
467  if(op.id()==ID_address_of)
468  {
469  if(op.operands().size()!=1 ||
470  (op.op0().id()!=ID_symbol &&
471  op.op0().id()!=ID_dynamic_object &&
472  op.op0().id()!=ID_string_constant))
473  return true;
474  }
475  else if(op.id()!=ID_constant ||
476  op.get(ID_value)!=ID_NULL)
477  return true;
478  }
479 
480  bool equal=expr.op0().op0()==expr.op1().op0();
481 
482  expr.make_bool(expr.id()==ID_equal?equal:!equal);
483 
484  return false;
485 }
486 
488 {
489  if(expr.operands().size()!=1)
490  return true;
491 
492  exprt &op=expr.op0();
493 
494  bool result=simplify_object(op);
495 
496  if(op.id()==ID_if)
497  {
498  const if_exprt &if_expr=to_if_expr(op);
499  exprt cond=if_expr.cond();
500 
501  exprt p_o_false=expr;
502  p_o_false.op0()=if_expr.false_case();
503 
504  expr.op0()=if_expr.true_case();
505 
506  expr=if_exprt(cond, expr, p_o_false, expr.type());
507  simplify_rec(expr);
508 
509  return false;
510  }
511 
512  return result;
513 }
514 
516 {
517  if(expr.operands().size()!=1)
518  return true;
519 
520  exprt &op=expr.op0();
521 
522  if(op.id()==ID_if && op.operands().size()==3)
523  {
524  if_exprt if_expr=lift_if(expr, 0);
527  simplify_if(if_expr);
528  expr.swap(if_expr);
529 
530  return false;
531  }
532 
533  bool result=true;
534 
535  if(!simplify_object(op))
536  result=false;
537 
538  // NULL is not dynamic
539  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
540  {
541  expr=false_exprt();
542  return false;
543  }
544 
545  // &something depends on the something
546  if(op.id()==ID_address_of && op.operands().size()==1)
547  {
548  if(op.op0().id()==ID_symbol)
549  {
550  const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
551 
552  // this is for the benefit of symex
553  expr.make_bool(has_prefix(id2string(identifier), "symex_dynamic::"));
554  return false;
555  }
556  else if(op.op0().id()==ID_string_constant)
557  {
558  expr=false_exprt();
559  return false;
560  }
561  else if(op.op0().id()==ID_array)
562  {
563  expr=false_exprt();
564  return false;
565  }
566  }
567 
568  return result;
569 }
570 
572 {
573  if(expr.operands().size()!=1)
574  return true;
575 
576  exprt &op=expr.op0();
577 
578  bool result=true;
579 
580  if(!simplify_object(op))
581  result=false;
582 
583  // NULL is not invalid
584  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
585  {
586  expr=false_exprt();
587  return false;
588  }
589 
590  // &anything is not invalid
591  if(op.id()==ID_address_of)
592  {
593  expr=false_exprt();
594  return false;
595  }
596 
597  return result;
598 }
599 
601 {
602  if(a==b)
603  return tvt(true);
604 
605  if(a.id()==ID_address_of && b.id()==ID_address_of &&
606  a.operands().size()==1 && b.operands().size()==1)
607  return objects_equal_address_of(a.op0(), b.op0());
608 
609  if(a.id()==ID_constant && b.id()==ID_constant &&
610  a.get(ID_value)==ID_NULL && b.get(ID_value)==ID_NULL)
611  return tvt(true);
612 
613  if(a.id()==ID_constant && b.id()==ID_address_of &&
614  a.get(ID_value)==ID_NULL)
615  return tvt(false);
616 
617  if(b.id()==ID_constant && a.id()==ID_address_of &&
618  b.get(ID_value)==ID_NULL)
619  return tvt(false);
620 
621  return tvt::unknown();
622 }
623 
625 {
626  if(a==b)
627  return tvt(true);
628 
629  if(a.id()==ID_symbol && b.id()==ID_symbol)
630  {
631  if(to_symbol_expr(a).get_identifier() == to_symbol_expr(b).get_identifier())
632  return tvt(true);
633  }
634  else if(a.id()==ID_index && b.id()==ID_index)
635  {
636  if(a.operands().size()==2 && b.operands().size()==2)
637  return objects_equal_address_of(a.op0(), b.op0());
638  }
639  else if(a.id()==ID_member && b.id()==ID_member)
640  {
641  if(a.operands().size()==1 && b.operands().size()==1)
642  return objects_equal_address_of(a.op0(), b.op0());
643  }
644 
645  return tvt::unknown();
646 }
647 
649 {
650  if(expr.operands().size()!=1)
651  return true;
652 
653  exprt &op=expr.op0();
654 
655  bool result=true;
656 
657  if(!simplify_object(op))
658  result=false;
659 
660  if(op.id()==ID_address_of && op.operands().size()==1)
661  {
662  if(op.op0().id()==ID_symbol)
663  {
664  // just get the type
665  const typet &type=ns.follow(op.op0().type());
666 
667  exprt size=size_of_expr(type, ns);
668 
669  if(size.is_not_nil())
670  {
671  const typet &expr_type = expr.type();
672 
673  if(size.type() != expr_type)
674  {
675  size.make_typecast(expr_type);
676  simplify_node(size);
677  }
678 
679  expr=size;
680  return false;
681  }
682  }
683  else if(op.op0().id()==ID_string_constant)
684  {
685  typet type=expr.type();
686  expr=from_integer(op.op0().get(ID_value).size()+1, type);
687  return false;
688  }
689  }
690 
691  return result;
692 }
693 
695 {
696  if(expr.operands().size()!=1)
697  return true;
698 
699  // we expand the definition
700  exprt def=good_pointer_def(expr.op0(), ns);
701 
702  // recursive call
703  simplify_node(def);
704 
705  expr.swap(def);
706 
707  return false;
708 }
simplify_exprt::simplify_node
bool simplify_node(exprt &expr)
Definition: simplify_expr.cpp:2113
exprt::op2
exprt & op2()
Definition: expr.h:90
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
pointer_offset_size.h
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:165
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
simplify_exprt::simplify_pointer_object
bool simplify_pointer_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:487
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
typet::subtype
const typet & subtype() const
Definition: type.h:38
simplify_exprt::simplify_inequality_pointer_object
bool simplify_inequality_pointer_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:454
simplify_expr_class.h
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:83
typet
The type of an expression, extends irept.
Definition: type.h:27
threeval.h
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
pointer_predicates.h
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:738
exprt::op0
exprt & op0()
Definition: expr.h:84
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
simplify_exprt::simplify_dynamic_object
bool simplify_dynamic_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:515
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
simplify_exprt::simplify_good_pointer
bool simplify_good_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:694
is_dereference_integer_object
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
Definition: simplify_expr_pointer.cpp:23
compute_pointer_offset
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:533
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
simplify_exprt::simplify_inequality_address_of
bool simplify_inequality_address_of(exprt &expr)
Definition: simplify_expr_pointer.cpp:413
size_of_expr
exprt size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:292
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:3380
simplify_exprt::simplify_invalid_pointer
bool simplify_invalid_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:571
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
simplify_exprt::simplify_object_size
bool simplify_object_size(exprt &expr)
Definition: simplify_expr_pointer.cpp:648
exprt::op1
exprt & op1()
Definition: expr.h:87
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
simplify_exprt::simplify_pointer_offset
bool simplify_pointer_offset(exprt &expr)
Definition: simplify_expr_pointer.cpp:211
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
tvt
Definition: threeval.h:19
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:425
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
simplify_exprt::objects_equal
static tvt objects_equal(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:600
simplify_exprt::objects_equal_address_of
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:624
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:90
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:20
simplify_exprt::simplify_address_of
bool simplify_address_of(exprt &expr)
Definition: simplify_expr_pointer.cpp:173
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
simplify_exprt::simplify_rec
bool simplify_rec(exprt &expr)
Definition: simplify_expr.cpp:2245
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
simplify_exprt::simplify_object
bool simplify_object(exprt &expr)
Definition: simplify_expr.cpp:1341
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:218
config.h
simplify_exprt::simplify_if
bool simplify_if(if_exprt &expr)
Definition: simplify_expr.cpp:1078
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:158
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
exprt::operands
operandst & operands()
Definition: expr.h:78
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
simplify_exprt::simplify_address_of_arg
bool simplify_address_of_arg(exprt &expr)
Definition: simplify_expr_pointer.cpp:52
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
c_types.h
dstringt::size
size_t size() const
Definition: dstring.h:91
validation_modet::INVARIANT
@ INVARIANT
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423