CBMC
pointer_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for Pointers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_POINTER_EXPR_H
10 #define CPROVER_UTIL_POINTER_EXPR_H
11 
14 
15 #include "bitvector_types.h"
16 #include "std_expr.h"
17 
18 class namespacet;
19 
24 {
25 public:
26  pointer_typet(typet _base_type, std::size_t width)
27  : bitvector_typet(ID_pointer, width)
28  {
29  add_subtype() = std::move(_base_type);
30  }
31 
35  const typet &base_type() const
36  {
37  return subtype();
38  }
39 
44  {
45  return subtype();
46  }
47 
48  // Use .base_type() instead -- this method will be removed
49  const typet &subtype() const
50  {
51  // The existence of get_sub() front is enforced by check(...)
52  return static_cast<const typet &>(get_sub().front());
53  }
54 
55  // Use .base_type() instead -- this method will be removed
57  {
58  // The existence of get_sub() front is enforced by check(...)
59  return static_cast<typet &>(get_sub().front());
60  }
61 
63  {
64  return signedbv_typet(get_width());
65  }
66 
67  static void check(
68  const typet &type,
70  {
71  bitvector_typet::check(type, vm);
73  }
74 };
75 
79 template <>
80 inline bool can_cast_type<pointer_typet>(const typet &type)
81 {
82  return type.id() == ID_pointer;
83 }
84 
93 inline const pointer_typet &to_pointer_type(const typet &type)
94 {
97  return static_cast<const pointer_typet &>(type);
98 }
99 
102 {
104  pointer_typet::check(type);
105  return static_cast<pointer_typet &>(type);
106 }
107 
110 inline bool is_void_pointer(const typet &type)
111 {
112  return type.id() == ID_pointer &&
113  to_pointer_type(type).base_type().id() == ID_empty;
114 }
115 
121 {
122 public:
123  reference_typet(typet _subtype, std::size_t _width)
124  : pointer_typet(std::move(_subtype), _width)
125  {
126  set(ID_C_reference, true);
127  }
128 
129  static void check(
130  const typet &type,
132  {
133  PRECONDITION(type.id() == ID_pointer);
134  DATA_CHECK(
135  vm, type.get_sub().size() == 1, "reference must have one type parameter");
137  static_cast<const reference_typet &>(type);
138  DATA_CHECK(
139  vm, !reference_type.get(ID_width).empty(), "reference must have width");
140  DATA_CHECK(
141  vm, reference_type.get_width() > 0, "reference must have non-zero width");
142  }
143 };
144 
148 template <>
149 inline bool can_cast_type<reference_typet>(const typet &type)
150 {
151  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
152 }
153 
162 inline const reference_typet &to_reference_type(const typet &type)
163 {
165  return static_cast<const reference_typet &>(type);
166 }
167 
170 {
172  return static_cast<reference_typet &>(type);
173 }
174 
175 bool is_reference(const typet &type);
176 
177 bool is_rvalue_reference(const typet &type);
178 
181 {
182 public:
184  : binary_exprt(
185  exprt(ID_unknown),
186  ID_object_descriptor,
187  exprt(ID_unknown),
188  typet())
189  {
190  }
191 
192  explicit object_descriptor_exprt(exprt _object)
193  : binary_exprt(
194  std::move(_object),
195  ID_object_descriptor,
196  exprt(ID_unknown),
197  typet())
198  {
199  }
200 
205  void build(const exprt &expr, const namespacet &ns);
206 
208  {
209  return op0();
210  }
211 
212  const exprt &object() const
213  {
214  return op0();
215  }
216 
217  static const exprt &root_object(const exprt &expr);
218  const exprt &root_object() const
219  {
220  return root_object(object());
221  }
222 
224  {
225  return op1();
226  }
227 
228  const exprt &offset() const
229  {
230  return op1();
231  }
232 };
233 
234 template <>
236 {
237  return base.id() == ID_object_descriptor;
238 }
239 
240 inline void validate_expr(const object_descriptor_exprt &value)
241 {
242  validate_operands(value, 2, "Object descriptor must have two operands");
243 }
244 
251 inline const object_descriptor_exprt &
253 {
254  PRECONDITION(expr.id() == ID_object_descriptor);
255  const object_descriptor_exprt &ret =
256  static_cast<const object_descriptor_exprt &>(expr);
257  validate_expr(ret);
258  return ret;
259 }
260 
263 {
264  PRECONDITION(expr.id() == ID_object_descriptor);
265  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
266  validate_expr(ret);
267  return ret;
268 }
269 
272 {
273 public:
275  : binary_exprt(
276  exprt(ID_unknown),
277  ID_dynamic_object,
278  exprt(ID_unknown),
279  std::move(type))
280  {
281  }
282 
283  void set_instance(unsigned int instance);
284 
285  unsigned int get_instance() const;
286 
288  {
289  return op1();
290  }
291 
292  const exprt &valid() const
293  {
294  return op1();
295  }
296 };
297 
298 template <>
300 {
301  return base.id() == ID_dynamic_object;
302 }
303 
304 inline void validate_expr(const dynamic_object_exprt &value)
305 {
306  validate_operands(value, 2, "Dynamic object must have two operands");
307 }
308 
316 {
317  PRECONDITION(expr.id() == ID_dynamic_object);
318  const dynamic_object_exprt &ret =
319  static_cast<const dynamic_object_exprt &>(expr);
320  validate_expr(ret);
321  return ret;
322 }
323 
326 {
327  PRECONDITION(expr.id() == ID_dynamic_object);
328  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
329  validate_expr(ret);
330  return ret;
331 }
332 
335 {
336 public:
338  : unary_predicate_exprt(ID_is_dynamic_object, op)
339  {
340  }
341 
343  {
344  return op();
345  }
346 
347  const exprt &address() const
348  {
349  return op();
350  }
351 };
352 
353 template <>
355 {
356  return base.id() == ID_is_dynamic_object;
357 }
358 
359 inline void validate_expr(const is_dynamic_object_exprt &value)
360 {
361  validate_operands(value, 1, "is_dynamic_object must have one operand");
362 }
363 
364 inline const is_dynamic_object_exprt &
366 {
367  PRECONDITION(expr.id() == ID_is_dynamic_object);
369  expr.operands().size() == 1, "is_dynamic_object must have one operand");
370  return static_cast<const is_dynamic_object_exprt &>(expr);
371 }
372 
376 {
377  PRECONDITION(expr.id() == ID_is_dynamic_object);
379  expr.operands().size() == 1, "is_dynamic_object must have one operand");
380  return static_cast<is_dynamic_object_exprt &>(expr);
381 }
382 
387 {
388 public:
390  : ternary_exprt(
391  ID_pointer_in_range,
392  std::move(a),
393  std::move(b),
394  std::move(c),
395  bool_typet())
396  {
397  PRECONDITION(op0().type().id() == ID_pointer);
398  PRECONDITION(op1().type().id() == ID_pointer);
399  PRECONDITION(op2().type().id() == ID_pointer);
400  }
401 
402  const exprt &lower_bound() const
403  {
404  return op0();
405  }
406 
407  const exprt &pointer() const
408  {
409  return op1();
410  }
411 
412  const exprt &upper_bound() const
413  {
414  return op2();
415  }
416 
417  // translate into equivalent conjunction
418  exprt lower() const;
419 };
420 
421 template <>
423 {
424  return base.id() == ID_pointer_in_range;
425 }
426 
427 inline void validate_expr(const pointer_in_range_exprt &value)
428 {
429  validate_operands(value, 3, "pointer_in_range must have three operands");
430 }
431 
433 {
434  PRECONDITION(expr.id() == ID_pointer_in_range);
436  expr.operands().size() == 3, "pointer_in_range must have three operands");
437  return static_cast<const pointer_in_range_exprt &>(expr);
438 }
439 
443 {
444  PRECONDITION(expr.id() == ID_pointer_in_range);
446  expr.operands().size() == 3, "pointer_in_range must have three operands");
447  return static_cast<pointer_in_range_exprt &>(expr);
448 }
449 
453 {
454 public:
456  exprt a,
457  exprt b,
458  exprt c,
459  exprt is_deallocated,
460  exprt is_dead)
461  : expr_protectedt(
462  ID_prophecy_pointer_in_range,
463  bool_typet{},
464  {std::move(a),
465  std::move(b),
466  std::move(c),
467  std::move(is_deallocated),
468  std::move(is_dead)})
469  {
470  PRECONDITION(op0().type().id() == ID_pointer);
471  PRECONDITION(op1().type().id() == ID_pointer);
472  PRECONDITION(op2().type().id() == ID_pointer);
473  }
474 
475  const exprt &lower_bound() const
476  {
477  return op0();
478  }
479 
480  const exprt &pointer() const
481  {
482  return op1();
483  }
484 
485  const exprt &upper_bound() const
486  {
487  return op2();
488  }
489 
490  const exprt &deallocated_ptr() const
491  {
492  return op3();
493  }
494 
495  const exprt &dead_ptr() const
496  {
497  return operands()[4];
498  }
499 
500  // translate into equivalent conjunction
501  exprt lower(const namespacet &ns) const;
502 };
503 
504 template <>
506 {
507  return base.id() == ID_prophecy_pointer_in_range;
508 }
509 
511 {
513  value, 5, "prophecy_pointer_in_range must have five operands");
514 }
515 
516 inline const prophecy_pointer_in_range_exprt &
518 {
519  PRECONDITION(expr.id() == ID_prophecy_pointer_in_range);
521  expr.operands().size() == 5,
522  "prophecy_pointer_in_range must have five operands");
523  return static_cast<const prophecy_pointer_in_range_exprt &>(expr);
524 }
525 
530 {
531  PRECONDITION(expr.id() == ID_prophecy_pointer_in_range);
533  expr.operands().size() == 5,
534  "prophecy_pointer_in_range must have five operands");
535  return static_cast<prophecy_pointer_in_range_exprt &>(expr);
536 }
537 
540 {
541 public:
542  explicit address_of_exprt(const exprt &op);
543 
545  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
546  {
547  }
548 
550  {
551  return op0();
552  }
553 
554  const exprt &object() const
555  {
556  return op0();
557  }
558 };
559 
560 template <>
561 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
562 {
563  return base.id() == ID_address_of;
564 }
565 
566 inline void validate_expr(const address_of_exprt &value)
567 {
568  validate_operands(value, 1, "Address of must have one operand");
569 }
570 
577 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
578 {
579  PRECONDITION(expr.id() == ID_address_of);
580  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
581  validate_expr(ret);
582  return ret;
583 }
584 
587 {
588  PRECONDITION(expr.id() == ID_address_of);
589  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
590  validate_expr(ret);
591  return ret;
592 }
593 
596 {
597 public:
598  explicit object_address_exprt(const symbol_exprt &);
599 
601 
603  {
604  return get(ID_identifier);
605  }
606 
607  const pointer_typet &type() const
608  {
609  return static_cast<const pointer_typet &>(exprt::type());
610  }
611 
613  {
614  return static_cast<pointer_typet &>(exprt::type());
615  }
616 
618  const typet &object_type() const
619  {
620  return type().base_type();
621  }
622 
623  symbol_exprt object_expr() const;
624 };
625 
626 template <>
628 {
629  return base.id() == ID_object_address;
630 }
631 
632 inline void validate_expr(const object_address_exprt &value)
633 {
634  validate_operands(value, 0, "object_address must have zero operands");
635 }
636 
644 {
645  PRECONDITION(expr.id() == ID_object_address);
646  const object_address_exprt &ret =
647  static_cast<const object_address_exprt &>(expr);
648  validate_expr(ret);
649  return ret;
650 }
651 
654 {
655  PRECONDITION(expr.id() == ID_object_address);
656  object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
657  validate_expr(ret);
658  return ret;
659 }
660 
664 {
665 public:
669  exprt base,
670  const irep_idt &component_name,
672 
674  {
675  return op0();
676  }
677 
678  const exprt &base() const
679  {
680  return op0();
681  }
682 
683  const pointer_typet &type() const
684  {
685  return static_cast<const pointer_typet &>(exprt::type());
686  }
687 
689  {
690  return static_cast<pointer_typet &>(exprt::type());
691  }
692 
694  const typet &field_type() const
695  {
696  return type().base_type();
697  }
698 
699  const typet &compound_type() const
700  {
701  return to_pointer_type(base().type()).base_type();
702  }
703 
704  const irep_idt &component_name() const
705  {
706  return get(ID_component_name);
707  }
708 };
709 
710 template <>
712 {
713  return expr.id() == ID_field_address;
714 }
715 
716 inline void validate_expr(const field_address_exprt &value)
717 {
718  validate_operands(value, 1, "field_address must have one operand");
719 }
720 
728 {
729  PRECONDITION(expr.id() == ID_field_address);
730  const field_address_exprt &ret =
731  static_cast<const field_address_exprt &>(expr);
732  validate_expr(ret);
733  return ret;
734 }
735 
738 {
739  PRECONDITION(expr.id() == ID_field_address);
740  field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
741  validate_expr(ret);
742  return ret;
743 }
744 
748 {
749 public:
754 
759 
760  const pointer_typet &type() const
761  {
762  return static_cast<const pointer_typet &>(exprt::type());
763  }
764 
766  {
767  return static_cast<pointer_typet &>(exprt::type());
768  }
769 
771  const typet &element_type() const
772  {
773  return type().base_type();
774  }
775 
777  {
778  return op0();
779  }
780 
781  const exprt &base() const
782  {
783  return op0();
784  }
785 
787  {
788  return op1();
789  }
790 
791  const exprt &index() const
792  {
793  return op1();
794  }
795 };
796 
797 template <>
799 {
800  return expr.id() == ID_element_address;
801 }
802 
803 inline void validate_expr(const element_address_exprt &value)
804 {
805  validate_operands(value, 2, "element_address must have two operands");
806 }
807 
815 {
816  PRECONDITION(expr.id() == ID_element_address);
817  const element_address_exprt &ret =
818  static_cast<const element_address_exprt &>(expr);
819  validate_expr(ret);
820  return ret;
821 }
822 
825 {
826  PRECONDITION(expr.id() == ID_element_address);
827  element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
828  validate_expr(ret);
829  return ret;
830 }
831 
834 {
835 public:
836  // The given operand must have pointer type.
837  explicit dereference_exprt(const exprt &op)
838  : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
839  {
840  }
841 
843  : unary_exprt(ID_dereference, std::move(op), std::move(type))
844  {
845  }
846 
848  {
849  return op0();
850  }
851 
852  const exprt &pointer() const
853  {
854  return op0();
855  }
856 
857  static void check(
858  const exprt &expr,
860  {
861  DATA_CHECK(
862  vm,
863  expr.operands().size() == 1,
864  "dereference expression must have one operand");
865  }
866 
867  static void validate(
868  const exprt &expr,
869  const namespacet &ns,
871 };
872 
873 template <>
874 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
875 {
876  return base.id() == ID_dereference;
877 }
878 
879 inline void validate_expr(const dereference_exprt &value)
880 {
881  validate_operands(value, 1, "Dereference must have one operand");
882 }
883 
890 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
891 {
892  PRECONDITION(expr.id() == ID_dereference);
893  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
894  validate_expr(ret);
895  return ret;
896 }
897 
900 {
901  PRECONDITION(expr.id() == ID_dereference);
902  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
903  validate_expr(ret);
904  return ret;
905 }
906 
909 {
910 public:
912  : constant_exprt(ID_NULL, std::move(type))
913  {
914  }
915 };
916 
920 {
921 public:
923  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
924  {
925  }
926 
927  const exprt &pointer() const
928  {
929  return op0();
930  }
931 
932  const exprt &size() const
933  {
934  return op1();
935  }
936 };
937 
938 template <>
939 inline bool can_cast_expr<r_or_w_ok_exprt>(const exprt &base)
940 {
941  return base.id() == ID_r_ok || base.id() == ID_w_ok || base.id() == ID_rw_ok;
942 }
943 
944 inline void validate_expr(const r_or_w_ok_exprt &value)
945 {
946  validate_operands(value, 2, "r_or_w_ok must have two operands");
947 }
948 
949 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
950 {
951  PRECONDITION(
952  expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
953  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
954  validate_expr(ret);
955  return ret;
956 }
957 
960 {
961 public:
963  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
964  {
965  }
966 };
967 
968 template <>
969 inline bool can_cast_expr<r_ok_exprt>(const exprt &base)
970 {
971  return base.id() == ID_r_ok;
972 }
973 
974 inline void validate_expr(const r_ok_exprt &value)
975 {
976  validate_operands(value, 2, "r_ok must have two operands");
977 }
978 
979 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
980 {
981  PRECONDITION(expr.id() == ID_r_ok);
982  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
983  validate_expr(ret);
984  return ret;
985 }
986 
989 {
990 public:
992  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
993  {
994  }
995 };
996 
997 template <>
998 inline bool can_cast_expr<w_ok_exprt>(const exprt &base)
999 {
1000  return base.id() == ID_w_ok;
1001 }
1002 
1003 inline void validate_expr(const w_ok_exprt &value)
1004 {
1005  validate_operands(value, 2, "w_ok must have two operands");
1006 }
1007 
1008 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
1009 {
1010  PRECONDITION(expr.id() == ID_w_ok);
1011  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
1012  validate_expr(ret);
1013  return ret;
1014 }
1015 
1019 {
1020 public:
1022  irep_idt id,
1023  exprt pointer,
1024  exprt size,
1025  exprt is_deallocated,
1026  exprt is_dead)
1027  : expr_protectedt(
1028  id,
1029  bool_typet{},
1030  {std::move(pointer),
1031  std::move(size),
1032  std::move(is_deallocated),
1033  std::move(is_dead)})
1034  {
1035  }
1036 
1039  id,
1040  std::move(pointer),
1041  std::move(size),
1042  nil_exprt{},
1043  nil_exprt{})
1044  {
1045  }
1046 
1047  const exprt &pointer() const
1048  {
1049  return op0();
1050  }
1051 
1052  const exprt &size() const
1053  {
1054  return op1();
1055  }
1056 
1057  const exprt &deallocated_ptr() const
1058  {
1059  return op2();
1060  }
1061 
1063  {
1064  return op2();
1065  }
1066 
1067  const exprt &dead_ptr() const
1068  {
1069  return op3();
1070  }
1071 
1073  {
1074  return op3();
1075  }
1076 
1079  exprt lower(const namespacet &ns) const;
1080 };
1081 
1082 template <>
1084 {
1085  return base.id() == ID_prophecy_r_ok || base.id() == ID_prophecy_w_ok ||
1086  base.id() == ID_prophecy_rw_ok;
1087 }
1088 
1089 inline void validate_expr(const prophecy_r_or_w_ok_exprt &value)
1090 {
1091  validate_operands(value, 4, "r_or_w_ok must have four operands");
1092 }
1093 
1094 inline const prophecy_r_or_w_ok_exprt &
1096 {
1097  PRECONDITION(
1098  expr.id() == ID_prophecy_r_ok || expr.id() == ID_prophecy_w_ok ||
1099  expr.id() == ID_prophecy_rw_ok);
1100  auto &ret = static_cast<const prophecy_r_or_w_ok_exprt &>(expr);
1101  validate_expr(ret);
1102  return ret;
1103 }
1104 
1107 {
1108 public:
1110  exprt pointer,
1111  exprt size,
1112  exprt is_deallocated,
1113  exprt is_dead)
1115  ID_prophecy_r_ok,
1116  std::move(pointer),
1117  std::move(size),
1118  std::move(is_deallocated),
1119  std::move(is_dead))
1120  {
1121  }
1122 
1125  std::move(pointer),
1126  std::move(size),
1127  nil_exprt{},
1128  nil_exprt{})
1129  {
1130  }
1131 };
1132 
1133 template <>
1135 {
1136  return base.id() == ID_prophecy_r_ok;
1137 }
1138 
1139 inline void validate_expr(const prophecy_r_ok_exprt &value)
1140 {
1141  validate_operands(value, 4, "r_ok must have four operands");
1142 }
1143 
1145 {
1146  PRECONDITION(expr.id() == ID_prophecy_r_ok);
1147  const prophecy_r_ok_exprt &ret =
1148  static_cast<const prophecy_r_ok_exprt &>(expr);
1149  validate_expr(ret);
1150  return ret;
1151 }
1152 
1155 {
1156 public:
1158  exprt pointer,
1159  exprt size,
1160  exprt is_deallocated,
1161  exprt is_dead)
1163  ID_prophecy_w_ok,
1164  std::move(pointer),
1165  std::move(size),
1166  std::move(is_deallocated),
1167  std::move(is_dead))
1168  {
1169  }
1170 
1173  std::move(pointer),
1174  std::move(size),
1175  nil_exprt{},
1176  nil_exprt{})
1177  {
1178  }
1179 };
1180 
1181 template <>
1183 {
1184  return base.id() == ID_prophecy_w_ok;
1185 }
1186 
1187 inline void validate_expr(const prophecy_w_ok_exprt &value)
1188 {
1189  validate_operands(value, 4, "w_ok must have four operands");
1190 }
1191 
1193 {
1194  PRECONDITION(expr.id() == ID_prophecy_w_ok);
1195  const prophecy_w_ok_exprt &ret =
1196  static_cast<const prophecy_w_ok_exprt &>(expr);
1197  validate_expr(ret);
1198  return ret;
1199 }
1200 
1210 {
1211 public:
1213  const irep_idt &_value,
1214  const exprt &_pointer)
1215  : unary_exprt(ID_annotated_pointer_constant, _pointer, _pointer.type())
1216  {
1217  set_value(_value);
1218  }
1219 
1220  const irep_idt &get_value() const
1221  {
1222  return get(ID_value);
1223  }
1224 
1225  void set_value(const irep_idt &value)
1226  {
1227  set(ID_value, value);
1228  }
1229 
1231  {
1232  return op0();
1233  }
1234 
1235  const exprt &symbolic_pointer() const
1236  {
1237  return op0();
1238  }
1239 };
1240 
1241 template <>
1243 {
1244  return base.id() == ID_annotated_pointer_constant;
1245 }
1246 
1248 {
1250  value, 1, "Annotated pointer constant must have one operand");
1251 }
1252 
1259 inline const annotated_pointer_constant_exprt &
1261 {
1262  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
1264  static_cast<const annotated_pointer_constant_exprt &>(expr);
1265  validate_expr(ret);
1266  return ret;
1267 }
1268 
1272 {
1273  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
1275  static_cast<annotated_pointer_constant_exprt &>(expr);
1276  validate_expr(ret);
1277  return ret;
1278 }
1279 
1282 {
1283 public:
1285  : unary_exprt(ID_pointer_offset, std::move(pointer), std::move(type))
1286  {
1287  }
1288 
1290  {
1291  return op0();
1292  }
1293 
1294  const exprt &pointer() const
1295  {
1296  return op0();
1297  }
1298 };
1299 
1300 template <>
1302 {
1303  return base.id() == ID_pointer_offset;
1304 }
1305 
1306 inline void validate_expr(const pointer_offset_exprt &value)
1307 {
1308  validate_operands(value, 1, "pointer_offset must have one operand");
1310  value.pointer().type().id() == ID_pointer,
1311  "pointer_offset must have pointer-typed operand");
1312 }
1313 
1321 {
1322  PRECONDITION(expr.id() == ID_pointer_offset);
1323  const pointer_offset_exprt &ret =
1324  static_cast<const pointer_offset_exprt &>(expr);
1325  validate_expr(ret);
1326  return ret;
1327 }
1328 
1331 {
1332  PRECONDITION(expr.id() == ID_pointer_offset);
1333  pointer_offset_exprt &ret = static_cast<pointer_offset_exprt &>(expr);
1334  validate_expr(ret);
1335  return ret;
1336 }
1337 
1340 {
1341 public:
1343  : unary_exprt(ID_pointer_object, std::move(pointer), std::move(type))
1344  {
1345  }
1346 
1348  {
1349  return op0();
1350  }
1351 
1352  const exprt &pointer() const
1353  {
1354  return op0();
1355  }
1356 };
1357 
1358 template <>
1360 {
1361  return base.id() == ID_pointer_object;
1362 }
1363 
1364 inline void validate_expr(const pointer_object_exprt &value)
1365 {
1366  validate_operands(value, 1, "pointer_object must have one operand");
1368  value.pointer().type().id() == ID_pointer,
1369  "pointer_object must have pointer-typed operand");
1370 }
1371 
1379 {
1380  PRECONDITION(expr.id() == ID_pointer_object);
1381  const pointer_object_exprt &ret =
1382  static_cast<const pointer_object_exprt &>(expr);
1383  validate_expr(ret);
1384  return ret;
1385 }
1386 
1389 {
1390  PRECONDITION(expr.id() == ID_pointer_object);
1391  pointer_object_exprt &ret = static_cast<pointer_object_exprt &>(expr);
1392  validate_expr(ret);
1393  return ret;
1394 }
1395 
1399 {
1400 public:
1402  : unary_exprt(ID_object_size, std::move(pointer), std::move(type))
1403  {
1404  }
1405 
1407  {
1408  return op();
1409  }
1410 
1411  const exprt &pointer() const
1412  {
1413  return op();
1414  }
1415 };
1416 
1423 inline const object_size_exprt &to_object_size_expr(const exprt &expr)
1424 {
1425  PRECONDITION(expr.id() == ID_object_size);
1426  const object_size_exprt &ret = static_cast<const object_size_exprt &>(expr);
1427  validate_expr(ret);
1428  return ret;
1429 }
1430 
1433 {
1434  PRECONDITION(expr.id() == ID_object_size);
1435  object_size_exprt &ret = static_cast<object_size_exprt &>(expr);
1436  validate_expr(ret);
1437  return ret;
1438 }
1439 
1440 template <>
1441 inline bool can_cast_expr<object_size_exprt>(const exprt &base)
1442 {
1443  return base.id() == ID_object_size;
1444 }
1445 
1446 inline void validate_expr(const object_size_exprt &value)
1447 {
1448  validate_operands(value, 1, "Object size expression must have one operand.");
1451  "Object size expression must have pointer typed operand.");
1452 }
1453 
1458 {
1459 public:
1461  : unary_predicate_exprt(ID_is_cstring, std::move(address))
1462  {
1463  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1464  }
1465 
1467  {
1468  return op0();
1469  }
1470 
1471  const exprt &address() const
1472  {
1473  return op0();
1474  }
1475 };
1476 
1477 template <>
1478 inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
1479 {
1480  return base.id() == ID_is_cstring;
1481 }
1482 
1483 inline void validate_expr(const is_cstring_exprt &value)
1484 {
1485  validate_operands(value, 1, "is_cstring must have one operand");
1486 }
1487 
1494 inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
1495 {
1496  PRECONDITION(expr.id() == ID_is_cstring);
1497  const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
1498  validate_expr(ret);
1499  return ret;
1500 }
1501 
1504 {
1505  PRECONDITION(expr.id() == ID_is_cstring);
1506  is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
1507  validate_expr(ret);
1508  return ret;
1509 }
1510 
1516 {
1517 public:
1519  : unary_exprt(ID_cstrlen, std::move(address), std::move(type))
1520  {
1521  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1522  }
1523 
1525  {
1526  return op0();
1527  }
1528 
1529  const exprt &address() const
1530  {
1531  return op0();
1532  }
1533 };
1534 
1535 template <>
1536 inline bool can_cast_expr<cstrlen_exprt>(const exprt &base)
1537 {
1538  return base.id() == ID_cstrlen;
1539 }
1540 
1541 inline void validate_expr(const cstrlen_exprt &value)
1542 {
1543  validate_operands(value, 1, "cstrlen must have one operand");
1544 }
1545 
1552 inline const cstrlen_exprt &to_cstrlen_expr(const exprt &expr)
1553 {
1554  PRECONDITION(expr.id() == ID_cstrlen);
1555  const cstrlen_exprt &ret = static_cast<const cstrlen_exprt &>(expr);
1556  validate_expr(ret);
1557  return ret;
1558 }
1559 
1562 {
1563  PRECONDITION(expr.id() == ID_cstrlen);
1564  cstrlen_exprt &ret = static_cast<cstrlen_exprt &>(expr);
1565  validate_expr(ret);
1566  return ret;
1567 }
1568 
1572 {
1573 public:
1575  : unary_predicate_exprt(ID_live_object, std::move(pointer))
1576  {
1577  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1578  }
1579 
1581  {
1582  return op0();
1583  }
1584 
1585  const exprt &pointer() const
1586  {
1587  return op0();
1588  }
1589 };
1590 
1591 template <>
1592 inline bool can_cast_expr<live_object_exprt>(const exprt &base)
1593 {
1594  return base.id() == ID_live_object;
1595 }
1596 
1597 inline void validate_expr(const live_object_exprt &value)
1598 {
1599  validate_operands(value, 1, "live_object must have one operand");
1600 }
1601 
1608 inline const live_object_exprt &to_live_object_expr(const exprt &expr)
1609 {
1610  PRECONDITION(expr.id() == ID_live_object);
1611  const live_object_exprt &ret = static_cast<const live_object_exprt &>(expr);
1612  validate_expr(ret);
1613  return ret;
1614 }
1615 
1618 {
1619  PRECONDITION(expr.id() == ID_live_object);
1620  live_object_exprt &ret = static_cast<live_object_exprt &>(expr);
1621  validate_expr(ret);
1622  return ret;
1623 }
1624 
1628 {
1629 public:
1631  : unary_predicate_exprt(ID_writeable_object, std::move(pointer))
1632  {
1633  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1634  }
1635 
1637  {
1638  return op0();
1639  }
1640 
1641  const exprt &pointer() const
1642  {
1643  return op0();
1644  }
1645 };
1646 
1647 template <>
1649 {
1650  return base.id() == ID_writeable_object;
1651 }
1652 
1653 inline void validate_expr(const writeable_object_exprt &value)
1654 {
1655  validate_operands(value, 1, "writeable_object must have one operand");
1656 }
1657 
1665 {
1666  PRECONDITION(expr.id() == ID_writeable_object);
1667  const writeable_object_exprt &ret =
1668  static_cast<const writeable_object_exprt &>(expr);
1669  validate_expr(ret);
1670  return ret;
1671 }
1672 
1675 {
1676  PRECONDITION(expr.id() == ID_writeable_object);
1677  writeable_object_exprt &ret = static_cast<writeable_object_exprt &>(expr);
1678  validate_expr(ret);
1679  return ret;
1680 }
1681 
1684 {
1685 public:
1686  explicit separate_exprt(exprt::operandst __operands)
1687  : multi_ary_exprt(ID_separate, std::move(__operands), bool_typet())
1688  {
1689  }
1690 
1692  : multi_ary_exprt(
1693  std::move(__op0),
1694  ID_separate,
1695  std::move(__op1),
1696  bool_typet())
1697  {
1698  }
1699 };
1700 
1701 template <>
1702 inline bool can_cast_expr<separate_exprt>(const exprt &base)
1703 {
1704  return base.id() == ID_separate;
1705 }
1706 
1707 inline void validate_expr(const separate_exprt &value)
1708 {
1709 }
1710 
1717 inline const separate_exprt &to_separate_expr(const exprt &expr)
1718 {
1719  PRECONDITION(expr.id() == ID_separate);
1720  const separate_exprt &ret = static_cast<const separate_exprt &>(expr);
1721  validate_expr(ret);
1722  return ret;
1723 }
1724 
1727 {
1728  PRECONDITION(expr.id() == ID_separate);
1729  separate_exprt &ret = static_cast<separate_exprt &>(expr);
1730  validate_expr(ret);
1731  return ret;
1732 }
1733 
1734 #endif // CPROVER_UTIL_POINTER_EXPR_H
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:240
Operator to return the address of an object.
Definition: pointer_expr.h:540
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:554
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:544
exprt & object()
Definition: pointer_expr.h:549
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
void set_value(const irep_idt &value)
const irep_idt & get_value() const
const exprt & symbolic_pointer() const
annotated_pointer_constant_exprt(const irep_idt &_value, const exprt &_pointer)
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
Base class of fixed-width bit-vector types.
Definition: std_types.h:909
std::size_t get_width() const
Definition: std_types.h:925
std::size_t width() const
Definition: std_types.cpp:158
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:939
The Boolean type.
Definition: std_types.h:36
A constant literal expression.
Definition: std_expr.h:2990
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
exprt & address()
const exprt & address() const
cstrlen_exprt(exprt address, typet type)
Operator to dereference a pointer.
Definition: pointer_expr.h:834
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:857
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:837
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
const exprt & pointer() const
Definition: pointer_expr.h:852
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:842
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Representation of heap-allocated objects.
Definition: pointer_expr.h:272
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:292
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:274
Operator to return the address of an array element relative to a base address.
Definition: pointer_expr.h:748
const exprt & index() const
Definition: pointer_expr.h:791
const exprt & base() const
Definition: pointer_expr.h:781
const pointer_typet & type() const
Definition: pointer_expr.h:760
element_address_exprt(const exprt &base, exprt index)
constructor for element addresses.
const typet & element_type() const
returns the type of the array element whose address is represented
Definition: pointer_expr.h:771
pointer_typet & type()
Definition: pointer_expr.h:765
Base class for all expressions.
Definition: expr.h:344
exprt & op3()
Definition: expr.h:142
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
Operator to return the address of a field relative to a base address.
Definition: pointer_expr.h:664
pointer_typet & type()
Definition: pointer_expr.h:688
const typet & compound_type() const
Definition: pointer_expr.h:699
const typet & field_type() const
returns the type of the field whose address is represented
Definition: pointer_expr.h:694
const exprt & base() const
Definition: pointer_expr.h:678
const pointer_typet & type() const
Definition: pointer_expr.h:683
const irep_idt & component_name() const
Definition: pointer_expr.h:704
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt & id() const
Definition: irep.h:388
A predicate that indicates that a zero-terminated string starts at the given address.
const exprt & address() const
is_cstring_exprt(exprt address)
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:335
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:337
const exprt & address() const
Definition: pointer_expr.h:347
A predicate that indicates that the object pointed to is live.
const exprt & pointer() const
live_object_exprt(exprt pointer)
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3081
The null pointer constant.
Definition: pointer_expr.h:909
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:911
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:596
symbol_exprt object_expr() const
const typet & object_type() const
returns the type of the object whose address is represented
Definition: pointer_expr.h:618
pointer_typet & type()
Definition: pointer_expr.h:612
const pointer_typet & type() const
Definition: pointer_expr.h:607
irep_idt object_identifier() const
Definition: pointer_expr.h:602
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:181
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:192
const exprt & object() const
Definition: pointer_expr.h:212
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
const exprt & root_object() const
Definition: pointer_expr.h:218
const exprt & offset() const
Definition: pointer_expr.h:228
Expression for finding the size (in bytes) of the object a pointer points to.
const exprt & pointer() const
object_size_exprt(exprt pointer, typet type)
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
Definition: pointer_expr.h:387
const exprt & lower_bound() const
Definition: pointer_expr.h:402
pointer_in_range_exprt(exprt a, exprt b, exprt c)
Definition: pointer_expr.h:389
const exprt & pointer() const
Definition: pointer_expr.h:407
const exprt & upper_bound() const
Definition: pointer_expr.h:412
A numerical identifier for the object a pointer points to.
pointer_object_exprt(exprt pointer, typet type)
const exprt & pointer() const
The offset (in bytes) of a pointer relative to the object.
const exprt & pointer() const
pointer_offset_exprt(exprt pointer, typet type)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:67
signedbv_typet difference_type() const
Definition: pointer_expr.h:62
const typet & subtype() const
Definition: pointer_expr.h:49
typet & base_type()
The type of the data what we point to.
Definition: pointer_expr.h:43
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
pointer_typet(typet _base_type, std::size_t width)
Definition: pointer_expr.h:26
typet & subtype()
Definition: pointer_expr.h:56
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
Definition: pointer_expr.h:453
const exprt & upper_bound() const
Definition: pointer_expr.h:485
const exprt & dead_ptr() const
Definition: pointer_expr.h:495
const exprt & lower_bound() const
Definition: pointer_expr.h:475
const exprt & pointer() const
Definition: pointer_expr.h:480
const exprt & deallocated_ptr() const
Definition: pointer_expr.h:490
exprt lower(const namespacet &ns) const
prophecy_pointer_in_range_exprt(exprt a, exprt b, exprt c, exprt is_deallocated, exprt is_dead)
Definition: pointer_expr.h:455
A predicate that indicates that an address range is ok to read.
prophecy_r_ok_exprt(exprt pointer, exprt size)
prophecy_r_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
A base class for a predicate that indicates that an address range is ok to read or write or both.
prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
const exprt & dead_ptr() const
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const exprt & size() const
const exprt & pointer() const
prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const exprt & deallocated_ptr() const
A predicate that indicates that an address range is ok to write.
prophecy_w_ok_exprt(exprt pointer, exprt size)
prophecy_w_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:960
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:962
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:920
const exprt & size() const
Definition: pointer_expr.h:932
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:922
const exprt & pointer() const
Definition: pointer_expr.h:927
The reference type.
Definition: pointer_expr.h:121
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:123
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:129
A predicate that indicates that the objects pointed to are distinct.
separate_exprt(exprt::operandst __operands)
separate_exprt(exprt __op0, exprt __op1)
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition: std_expr.h:131
An expression with three operands.
Definition: std_expr.h:67
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:199
The type of an expression, extends irept.
Definition: type.h:29
typet & add_subtype()
Definition: type.h:53
Generic base class for unary expressions.
Definition: std_expr.h:361
const exprt & op() const
Definition: std_expr.h:391
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:989
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:991
A predicate that indicates that the object pointed to is writeable.
const exprt & pointer() const
writeable_object_exprt(exprt pointer)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
bool can_cast_expr< separate_exprt >(const exprt &base)
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:240
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:149
const separate_exprt & to_separate_expr(const exprt &expr)
Cast an exprt to a separate_exprt.
bool can_cast_expr< field_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:711
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:110
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:949
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
const prophecy_w_ok_exprt & to_prophecy_w_ok_expr(const exprt &expr)
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)
Cast an exprt to a is_cstring_exprt.
const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr(const exprt &expr)
Definition: pointer_expr.h:517
bool can_cast_expr< prophecy_w_ok_exprt >(const exprt &base)
bool can_cast_expr< live_object_exprt >(const exprt &base)
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:145
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:299
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:727
bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)
Definition: pointer_expr.h:422
bool can_cast_expr< prophecy_pointer_in_range_exprt >(const exprt &base)
Definition: pointer_expr.h:505
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:874
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:152
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:354
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
bool can_cast_expr< cstrlen_exprt >(const exprt &base)
const prophecy_r_ok_exprt & to_prophecy_r_ok_expr(const exprt &expr)
bool can_cast_expr< object_address_exprt >(const exprt &base)
Definition: pointer_expr.h:627
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
bool can_cast_expr< object_size_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
bool can_cast_expr< is_cstring_exprt >(const exprt &base)
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:561
bool can_cast_expr< pointer_offset_exprt >(const exprt &base)
bool can_cast_expr< w_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:998
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:162
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:252
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:365
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
bool can_cast_expr< element_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:798
bool can_cast_expr< r_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:969
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
Definition: pointer_expr.h:432
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:643
bool can_cast_expr< r_or_w_ok_exprt >(const exprt &base)
Definition: pointer_expr.h:939
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:235
const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:315
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:979
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:814
bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)
bool can_cast_expr< writeable_object_exprt >(const exprt &base)
bool can_cast_expr< pointer_object_exprt >(const exprt &base)
bool can_cast_expr< prophecy_r_ok_exprt >(const exprt &base)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet