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  subtype().swap(_base_type);
30  }
31 
35  const typet &base_type() const
36  {
37  return subtype();
38  }
39 
44  {
45  return subtype();
46  }
47 
49  {
50  return signedbv_typet(get_width());
51  }
52 
53  static void check(
54  const typet &type,
56  {
58  DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
59  }
60 };
61 
65 template <>
66 inline bool can_cast_type<pointer_typet>(const typet &type)
67 {
68  return type.id() == ID_pointer;
69 }
70 
79 inline const pointer_typet &to_pointer_type(const typet &type)
80 {
83  return static_cast<const pointer_typet &>(type);
84 }
85 
88 {
91  return static_cast<pointer_typet &>(type);
92 }
93 
96 inline bool is_void_pointer(const typet &type)
97 {
98  return type.id() == ID_pointer &&
99  to_pointer_type(type).base_type().id() == ID_empty;
100 }
101 
107 {
108 public:
109  reference_typet(typet _subtype, std::size_t _width)
110  : pointer_typet(std::move(_subtype), _width)
111  {
112  set(ID_C_reference, true);
113  }
114 
115  static void check(
116  const typet &type,
118  {
119  PRECONDITION(type.id() == ID_pointer);
120  DATA_CHECK(
121  vm, type.get_sub().size() == 1, "reference must have one type parameter");
123  static_cast<const reference_typet &>(type);
124  DATA_CHECK(
125  vm, !reference_type.get(ID_width).empty(), "reference must have width");
126  DATA_CHECK(
127  vm, reference_type.get_width() > 0, "reference must have non-zero width");
128  }
129 };
130 
134 template <>
135 inline bool can_cast_type<reference_typet>(const typet &type)
136 {
137  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
138 }
139 
148 inline const reference_typet &to_reference_type(const typet &type)
149 {
151  return static_cast<const reference_typet &>(type);
152 }
153 
156 {
158  return static_cast<reference_typet &>(type);
159 }
160 
161 bool is_reference(const typet &type);
162 
163 bool is_rvalue_reference(const typet &type);
164 
167 {
168 public:
170  : binary_exprt(
171  exprt(ID_unknown),
172  ID_object_descriptor,
173  exprt(ID_unknown),
174  typet())
175  {
176  }
177 
178  explicit object_descriptor_exprt(exprt _object)
179  : binary_exprt(
180  std::move(_object),
181  ID_object_descriptor,
182  exprt(ID_unknown),
183  typet())
184  {
185  }
186 
191  void build(const exprt &expr, const namespacet &ns);
192 
194  {
195  return op0();
196  }
197 
198  const exprt &object() const
199  {
200  return op0();
201  }
202 
203  static const exprt &root_object(const exprt &expr);
204  const exprt &root_object() const
205  {
206  return root_object(object());
207  }
208 
210  {
211  return op1();
212  }
213 
214  const exprt &offset() const
215  {
216  return op1();
217  }
218 };
219 
220 template <>
222 {
223  return base.id() == ID_object_descriptor;
224 }
225 
226 inline void validate_expr(const object_descriptor_exprt &value)
227 {
228  validate_operands(value, 2, "Object descriptor must have two operands");
229 }
230 
237 inline const object_descriptor_exprt &
239 {
240  PRECONDITION(expr.id() == ID_object_descriptor);
241  const object_descriptor_exprt &ret =
242  static_cast<const object_descriptor_exprt &>(expr);
243  validate_expr(ret);
244  return ret;
245 }
246 
249 {
250  PRECONDITION(expr.id() == ID_object_descriptor);
251  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
252  validate_expr(ret);
253  return ret;
254 }
255 
258 {
259 public:
261  : binary_exprt(
262  exprt(ID_unknown),
263  ID_dynamic_object,
264  exprt(ID_unknown),
265  std::move(type))
266  {
267  }
268 
269  void set_instance(unsigned int instance);
270 
271  unsigned int get_instance() const;
272 
274  {
275  return op1();
276  }
277 
278  const exprt &valid() const
279  {
280  return op1();
281  }
282 };
283 
284 template <>
286 {
287  return base.id() == ID_dynamic_object;
288 }
289 
290 inline void validate_expr(const dynamic_object_exprt &value)
291 {
292  validate_operands(value, 2, "Dynamic object must have two operands");
293 }
294 
302 {
303  PRECONDITION(expr.id() == ID_dynamic_object);
304  const dynamic_object_exprt &ret =
305  static_cast<const dynamic_object_exprt &>(expr);
306  validate_expr(ret);
307  return ret;
308 }
309 
312 {
313  PRECONDITION(expr.id() == ID_dynamic_object);
314  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
315  validate_expr(ret);
316  return ret;
317 }
318 
321 {
322 public:
324  : unary_predicate_exprt(ID_is_dynamic_object, op)
325  {
326  }
327 
329  {
330  return op();
331  }
332 
333  const exprt &address() const
334  {
335  return op();
336  }
337 };
338 
339 template <>
341 {
342  return base.id() == ID_is_dynamic_object;
343 }
344 
345 inline void validate_expr(const is_dynamic_object_exprt &value)
346 {
347  validate_operands(value, 1, "is_dynamic_object must have one operand");
348 }
349 
350 inline const is_dynamic_object_exprt &
352 {
353  PRECONDITION(expr.id() == ID_is_dynamic_object);
355  expr.operands().size() == 1, "is_dynamic_object must have one operand");
356  return static_cast<const is_dynamic_object_exprt &>(expr);
357 }
358 
362 {
363  PRECONDITION(expr.id() == ID_is_dynamic_object);
365  expr.operands().size() == 1, "is_dynamic_object must have one operand");
366  return static_cast<is_dynamic_object_exprt &>(expr);
367 }
368 
373 {
374 public:
376  : ternary_exprt(
377  ID_pointer_in_range,
378  std::move(a),
379  std::move(b),
380  std::move(c),
381  bool_typet())
382  {
383  PRECONDITION(op0().type().id() == ID_pointer);
384  PRECONDITION(op1().type().id() == ID_pointer);
385  PRECONDITION(op2().type().id() == ID_pointer);
386  }
387 
388  // translate into equivalent conjunction
389  exprt lower() const;
390 };
391 
392 template <>
394 {
395  return base.id() == ID_pointer_in_range;
396 }
397 
398 inline void validate_expr(const pointer_in_range_exprt &value)
399 {
400  validate_operands(value, 3, "pointer_in_range must have three operands");
401 }
402 
404 {
405  PRECONDITION(expr.id() == ID_pointer_in_range);
407  expr.operands().size() == 3, "pointer_in_range must have three operands");
408  return static_cast<const pointer_in_range_exprt &>(expr);
409 }
410 
414 {
415  PRECONDITION(expr.id() == ID_pointer_in_range);
417  expr.operands().size() == 3, "pointer_in_range must have one operand");
418  return static_cast<pointer_in_range_exprt &>(expr);
419 }
420 
423 {
424 public:
425  explicit address_of_exprt(const exprt &op);
426 
428  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
429  {
430  }
431 
433  {
434  return op0();
435  }
436 
437  const exprt &object() const
438  {
439  return op0();
440  }
441 };
442 
443 template <>
444 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
445 {
446  return base.id() == ID_address_of;
447 }
448 
449 inline void validate_expr(const address_of_exprt &value)
450 {
451  validate_operands(value, 1, "Address of must have one operand");
452 }
453 
460 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
461 {
462  PRECONDITION(expr.id() == ID_address_of);
463  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
464  validate_expr(ret);
465  return ret;
466 }
467 
470 {
471  PRECONDITION(expr.id() == ID_address_of);
472  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
473  validate_expr(ret);
474  return ret;
475 }
476 
479 {
480 public:
481  explicit object_address_exprt(const symbol_exprt &);
482 
484 
486  {
487  return get(ID_identifier);
488  }
489 
490  const pointer_typet &type() const
491  {
492  return static_cast<const pointer_typet &>(exprt::type());
493  }
494 
496  {
497  return static_cast<pointer_typet &>(exprt::type());
498  }
499 
501  const typet &object_type() const
502  {
503  return type().base_type();
504  }
505 
506  symbol_exprt object_expr() const;
507 };
508 
509 template <>
511 {
512  return base.id() == ID_object_address;
513 }
514 
515 inline void validate_expr(const object_address_exprt &value)
516 {
517  validate_operands(value, 0, "object_address must have zero operands");
518 }
519 
527 {
528  PRECONDITION(expr.id() == ID_object_address);
529  const object_address_exprt &ret =
530  static_cast<const object_address_exprt &>(expr);
531  validate_expr(ret);
532  return ret;
533 }
534 
537 {
538  PRECONDITION(expr.id() == ID_object_address);
539  object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
540  validate_expr(ret);
541  return ret;
542 }
543 
547 {
548 public:
552  exprt base,
553  const irep_idt &component_name,
555 
557  {
558  return op0();
559  }
560 
561  const exprt &base() const
562  {
563  return op0();
564  }
565 
566  const pointer_typet &type() const
567  {
568  return static_cast<const pointer_typet &>(exprt::type());
569  }
570 
572  {
573  return static_cast<pointer_typet &>(exprt::type());
574  }
575 
577  const typet &field_type() const
578  {
579  return type().base_type();
580  }
581 
582  const typet &compound_type() const
583  {
584  return to_pointer_type(base().type()).base_type();
585  }
586 
587  const irep_idt &component_name() const
588  {
589  return get(ID_component_name);
590  }
591 };
592 
593 template <>
595 {
596  return expr.id() == ID_field_address;
597 }
598 
599 inline void validate_expr(const field_address_exprt &value)
600 {
601  validate_operands(value, 1, "field_address must have one operand");
602 }
603 
611 {
612  PRECONDITION(expr.id() == ID_field_address);
613  const field_address_exprt &ret =
614  static_cast<const field_address_exprt &>(expr);
615  validate_expr(ret);
616  return ret;
617 }
618 
621 {
622  PRECONDITION(expr.id() == ID_field_address);
623  field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
624  validate_expr(ret);
625  return ret;
626 }
627 
631 {
632 public:
637 
642 
643  const pointer_typet &type() const
644  {
645  return static_cast<const pointer_typet &>(exprt::type());
646  }
647 
649  {
650  return static_cast<pointer_typet &>(exprt::type());
651  }
652 
654  const typet &element_type() const
655  {
656  return type().base_type();
657  }
658 
660  {
661  return op0();
662  }
663 
664  const exprt &base() const
665  {
666  return op0();
667  }
668 
670  {
671  return op1();
672  }
673 
674  const exprt &index() const
675  {
676  return op1();
677  }
678 };
679 
680 template <>
682 {
683  return expr.id() == ID_element_address;
684 }
685 
686 inline void validate_expr(const element_address_exprt &value)
687 {
688  validate_operands(value, 2, "element_address must have two operands");
689 }
690 
698 {
699  PRECONDITION(expr.id() == ID_element_address);
700  const element_address_exprt &ret =
701  static_cast<const element_address_exprt &>(expr);
702  validate_expr(ret);
703  return ret;
704 }
705 
708 {
709  PRECONDITION(expr.id() == ID_element_address);
710  element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
711  validate_expr(ret);
712  return ret;
713 }
714 
717 {
718 public:
719  // The given operand must have pointer type.
720  explicit dereference_exprt(const exprt &op)
721  : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
722  {
723  }
724 
726  : unary_exprt(ID_dereference, std::move(op), std::move(type))
727  {
728  }
729 
731  {
732  return op0();
733  }
734 
735  const exprt &pointer() const
736  {
737  return op0();
738  }
739 
740  static void check(
741  const exprt &expr,
743  {
744  DATA_CHECK(
745  vm,
746  expr.operands().size() == 1,
747  "dereference expression must have one operand");
748  }
749 
750  static void validate(
751  const exprt &expr,
752  const namespacet &ns,
754 };
755 
756 template <>
757 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
758 {
759  return base.id() == ID_dereference;
760 }
761 
762 inline void validate_expr(const dereference_exprt &value)
763 {
764  validate_operands(value, 1, "Dereference must have one operand");
765 }
766 
773 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
774 {
775  PRECONDITION(expr.id() == ID_dereference);
776  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
777  validate_expr(ret);
778  return ret;
779 }
780 
783 {
784  PRECONDITION(expr.id() == ID_dereference);
785  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
786  validate_expr(ret);
787  return ret;
788 }
789 
792 {
793 public:
795  : constant_exprt(ID_NULL, std::move(type))
796  {
797  }
798 };
799 
803 {
804 public:
806  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
807  {
808  }
809 
810  const exprt &pointer() const
811  {
812  return op0();
813  }
814 
815  const exprt &size() const
816  {
817  return op1();
818  }
819 };
820 
821 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
822 {
823  PRECONDITION(
824  expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
825  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
826  validate_expr(ret);
827  return ret;
828 }
829 
832 {
833 public:
835  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
836  {
837  }
838 };
839 
840 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
841 {
842  PRECONDITION(expr.id() == ID_r_ok);
843  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
844  validate_expr(ret);
845  return ret;
846 }
847 
850 {
851 public:
853  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
854  {
855  }
856 };
857 
858 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
859 {
860  PRECONDITION(expr.id() == ID_w_ok);
861  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
862  validate_expr(ret);
863  return ret;
864 }
865 
875 {
876 public:
878  const irep_idt &_value,
879  const exprt &_pointer)
880  : unary_exprt(ID_annotated_pointer_constant, _pointer, _pointer.type())
881  {
882  set_value(_value);
883  }
884 
885  const irep_idt &get_value() const
886  {
887  return get(ID_value);
888  }
889 
890  void set_value(const irep_idt &value)
891  {
892  set(ID_value, value);
893  }
894 
896  {
897  return op0();
898  }
899 
900  const exprt &symbolic_pointer() const
901  {
902  return op0();
903  }
904 };
905 
906 template <>
908 {
909  return base.id() == ID_annotated_pointer_constant;
910 }
911 
913 {
915  value, 1, "Annotated pointer constant must have one operand");
916 }
917 
926 {
927  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
929  static_cast<const annotated_pointer_constant_exprt &>(expr);
930  validate_expr(ret);
931  return ret;
932 }
933 
937 {
938  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
940  static_cast<annotated_pointer_constant_exprt &>(expr);
941  validate_expr(ret);
942  return ret;
943 }
944 
947 {
948 public:
950  : unary_exprt(ID_pointer_offset, std::move(pointer), std::move(type))
951  {
952  }
953 
955  {
956  return op0();
957  }
958 
959  const exprt &pointer() const
960  {
961  return op0();
962  }
963 };
964 
965 template <>
967 {
968  return base.id() == ID_pointer_offset;
969 }
970 
971 inline void validate_expr(const pointer_offset_exprt &value)
972 {
973  validate_operands(value, 1, "pointer_offset must have one operand");
975  value.pointer().type().id() == ID_pointer,
976  "pointer_offset must have pointer-typed operand");
977 }
978 
986 {
987  PRECONDITION(expr.id() == ID_pointer_offset);
988  const pointer_offset_exprt &ret =
989  static_cast<const pointer_offset_exprt &>(expr);
990  validate_expr(ret);
991  return ret;
992 }
993 
996 {
997  PRECONDITION(expr.id() == ID_pointer_offset);
998  pointer_offset_exprt &ret = static_cast<pointer_offset_exprt &>(expr);
999  validate_expr(ret);
1000  return ret;
1001 }
1002 
1005 {
1006 public:
1008  : unary_exprt(ID_pointer_object, std::move(pointer), std::move(type))
1009  {
1010  }
1011 
1013  {
1014  return op0();
1015  }
1016 
1017  const exprt &pointer() const
1018  {
1019  return op0();
1020  }
1021 };
1022 
1023 template <>
1025 {
1026  return base.id() == ID_pointer_object;
1027 }
1028 
1029 inline void validate_expr(const pointer_object_exprt &value)
1030 {
1031  validate_operands(value, 1, "pointer_object must have one operand");
1033  value.pointer().type().id() == ID_pointer,
1034  "pointer_object must have pointer-typed operand");
1035 }
1036 
1044 {
1045  PRECONDITION(expr.id() == ID_pointer_object);
1046  const pointer_object_exprt &ret =
1047  static_cast<const pointer_object_exprt &>(expr);
1048  validate_expr(ret);
1049  return ret;
1050 }
1051 
1054 {
1055  PRECONDITION(expr.id() == ID_pointer_object);
1056  pointer_object_exprt &ret = static_cast<pointer_object_exprt &>(expr);
1057  validate_expr(ret);
1058  return ret;
1059 }
1060 
1064 {
1065 public:
1067  : unary_exprt(ID_object_size, std::move(pointer), std::move(type))
1068  {
1069  }
1070 
1072  {
1073  return op();
1074  }
1075 
1076  const exprt &pointer() const
1077  {
1078  return op();
1079  }
1080 };
1081 
1088 inline const object_size_exprt &to_object_size_expr(const exprt &expr)
1089 {
1090  PRECONDITION(expr.id() == ID_object_size);
1091  const object_size_exprt &ret = static_cast<const object_size_exprt &>(expr);
1092  validate_expr(ret);
1093  return ret;
1094 }
1095 
1098 {
1099  PRECONDITION(expr.id() == ID_object_size);
1100  object_size_exprt &ret = static_cast<object_size_exprt &>(expr);
1101  validate_expr(ret);
1102  return ret;
1103 }
1104 
1105 template <>
1106 inline bool can_cast_expr<object_size_exprt>(const exprt &base)
1107 {
1108  return base.id() == ID_object_size;
1109 }
1110 
1111 inline void validate_expr(const object_size_exprt &value)
1112 {
1113  validate_operands(value, 1, "Object size expression must have one operand.");
1116  "Object size expression must have pointer typed operand.");
1117 }
1118 
1123 {
1124 public:
1126  : unary_predicate_exprt(ID_is_cstring, std::move(address))
1127  {
1128  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1129  }
1130 
1132  {
1133  return op0();
1134  }
1135 
1136  const exprt &address() const
1137  {
1138  return op0();
1139  }
1140 };
1141 
1142 template <>
1143 inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
1144 {
1145  return base.id() == ID_is_cstring;
1146 }
1147 
1148 inline void validate_expr(const is_cstring_exprt &value)
1149 {
1150  validate_operands(value, 1, "is_cstring must have one operand");
1151 }
1152 
1159 inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
1160 {
1161  PRECONDITION(expr.id() == ID_is_cstring);
1162  const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
1163  validate_expr(ret);
1164  return ret;
1165 }
1166 
1169 {
1170  PRECONDITION(expr.id() == ID_is_cstring);
1171  is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
1172  validate_expr(ret);
1173  return ret;
1174 }
1175 
1181 {
1182 public:
1184  : unary_exprt(ID_cstrlen, std::move(address), std::move(type))
1185  {
1186  PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1187  }
1188 
1190  {
1191  return op0();
1192  }
1193 
1194  const exprt &address() const
1195  {
1196  return op0();
1197  }
1198 };
1199 
1200 template <>
1201 inline bool can_cast_expr<cstrlen_exprt>(const exprt &base)
1202 {
1203  return base.id() == ID_cstrlen;
1204 }
1205 
1206 inline void validate_expr(const cstrlen_exprt &value)
1207 {
1208  validate_operands(value, 1, "cstrlen must have one operand");
1209 }
1210 
1217 inline const cstrlen_exprt &to_cstrlen_expr(const exprt &expr)
1218 {
1219  PRECONDITION(expr.id() == ID_cstrlen);
1220  const cstrlen_exprt &ret = static_cast<const cstrlen_exprt &>(expr);
1221  validate_expr(ret);
1222  return ret;
1223 }
1224 
1227 {
1228  PRECONDITION(expr.id() == ID_cstrlen);
1229  cstrlen_exprt &ret = static_cast<cstrlen_exprt &>(expr);
1230  validate_expr(ret);
1231  return ret;
1232 }
1233 
1237 {
1238 public:
1240  : unary_predicate_exprt(ID_live_object, std::move(pointer))
1241  {
1242  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1243  }
1244 
1246  {
1247  return op0();
1248  }
1249 
1250  const exprt &pointer() const
1251  {
1252  return op0();
1253  }
1254 };
1255 
1256 template <>
1257 inline bool can_cast_expr<live_object_exprt>(const exprt &base)
1258 {
1259  return base.id() == ID_live_object;
1260 }
1261 
1262 inline void validate_expr(const live_object_exprt &value)
1263 {
1264  validate_operands(value, 1, "live_object must have one operand");
1265 }
1266 
1273 inline const live_object_exprt &to_live_object_expr(const exprt &expr)
1274 {
1275  PRECONDITION(expr.id() == ID_live_object);
1276  const live_object_exprt &ret = static_cast<const live_object_exprt &>(expr);
1277  validate_expr(ret);
1278  return ret;
1279 }
1280 
1283 {
1284  PRECONDITION(expr.id() == ID_live_object);
1285  live_object_exprt &ret = static_cast<live_object_exprt &>(expr);
1286  validate_expr(ret);
1287  return ret;
1288 }
1289 
1293 {
1294 public:
1296  : unary_predicate_exprt(ID_writeable_object, std::move(pointer))
1297  {
1298  PRECONDITION(as_const(*this).pointer().type().id() == ID_pointer);
1299  }
1300 
1302  {
1303  return op0();
1304  }
1305 
1306  const exprt &pointer() const
1307  {
1308  return op0();
1309  }
1310 };
1311 
1312 template <>
1314 {
1315  return base.id() == ID_writeable_object;
1316 }
1317 
1318 inline void validate_expr(const writeable_object_exprt &value)
1319 {
1320  validate_operands(value, 1, "writeable_object must have one operand");
1321 }
1322 
1330 {
1331  PRECONDITION(expr.id() == ID_writeable_object);
1332  const writeable_object_exprt &ret =
1333  static_cast<const writeable_object_exprt &>(expr);
1334  validate_expr(ret);
1335  return ret;
1336 }
1337 
1340 {
1341  PRECONDITION(expr.id() == ID_writeable_object);
1342  writeable_object_exprt &ret = static_cast<writeable_object_exprt &>(expr);
1343  validate_expr(ret);
1344  return ret;
1345 }
1346 
1349 {
1350 public:
1351  explicit separate_exprt(exprt::operandst __operands)
1352  : multi_ary_exprt(ID_separate, std::move(__operands), bool_typet())
1353  {
1354  }
1355 
1357  : multi_ary_exprt(
1358  std::move(__op0),
1359  ID_separate,
1360  std::move(__op1),
1361  bool_typet())
1362  {
1363  }
1364 };
1365 
1366 template <>
1367 inline bool can_cast_expr<separate_exprt>(const exprt &base)
1368 {
1369  return base.id() == ID_separate;
1370 }
1371 
1372 inline void validate_expr(const separate_exprt &value)
1373 {
1374 }
1375 
1382 inline const separate_exprt &to_separate_expr(const exprt &expr)
1383 {
1384  PRECONDITION(expr.id() == ID_separate);
1385  const separate_exprt &ret = static_cast<const separate_exprt &>(expr);
1386  validate_expr(ret);
1387  return ret;
1388 }
1389 
1392 {
1393  PRECONDITION(expr.id() == ID_separate);
1394  separate_exprt &ret = static_cast<separate_exprt &>(expr);
1395  validate_expr(ret);
1396  return ret;
1397 }
1398 
1399 #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:245
Operator to return the address of an object.
Definition: pointer_expr.h:423
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:437
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:427
exprt & object()
Definition: pointer_expr.h:432
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
Definition: pointer_expr.h:875
void set_value(const irep_idt &value)
Definition: pointer_expr.h:890
const irep_idt & get_value() const
Definition: pointer_expr.h:885
const exprt & symbolic_pointer() const
Definition: pointer_expr.h:900
annotated_pointer_constant_exprt(const irep_idt &_value, const exprt &_pointer)
Definition: pointer_expr.h:877
A base class for binary expressions.
Definition: std_expr.h:583
exprt & op1()
Definition: expr.h:128
exprt & op0()
Definition: expr.h:125
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:676
Base class of fixed-width bit-vector types.
Definition: std_types.h:865
std::size_t get_width() const
Definition: std_types.h:876
The Boolean type.
Definition: std_types.h:36
A constant literal expression.
Definition: std_expr.h:2942
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:717
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:740
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:720
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:735
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:725
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
bool empty() const
Definition: dstring.h:90
Representation of heap-allocated objects.
Definition: pointer_expr.h:258
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:278
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:260
Operator to return the address of an array element relative to a base address.
Definition: pointer_expr.h:631
const exprt & index() const
Definition: pointer_expr.h:674
const exprt & base() const
Definition: pointer_expr.h:664
const pointer_typet & type() const
Definition: pointer_expr.h:643
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:654
pointer_typet & type()
Definition: pointer_expr.h:648
exprt & op0()
Definition: expr.h:125
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:547
pointer_typet & type()
Definition: pointer_expr.h:571
const typet & compound_type() const
Definition: pointer_expr.h:582
const typet & field_type() const
returns the type of the field whose address is represented
Definition: pointer_expr.h:577
const exprt & base() const
Definition: pointer_expr.h:561
const pointer_typet & type() const
Definition: pointer_expr.h:566
const irep_idt & component_name() const
Definition: pointer_expr.h:587
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:456
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:420
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
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:321
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:323
const exprt & address() const
Definition: pointer_expr.h:333
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:857
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:792
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:794
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:479
symbol_exprt object_expr() const
const typet & object_type() const
returns the type of the object whose address is represented
Definition: pointer_expr.h:501
pointer_typet & type()
Definition: pointer_expr.h:495
const pointer_typet & type() const
Definition: pointer_expr.h:490
irep_idt object_identifier() const
Definition: pointer_expr.h:485
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:178
const exprt & object() const
Definition: pointer_expr.h:198
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:204
const exprt & offset() const
Definition: pointer_expr.h:214
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:373
pointer_in_range_exprt(exprt a, exprt b, exprt c)
Definition: pointer_expr.h:375
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.
Definition: pointer_expr.h:947
const exprt & pointer() const
Definition: pointer_expr.h:959
pointer_offset_exprt(exprt pointer, typet type)
Definition: pointer_expr.h:949
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:53
signedbv_typet difference_type() const
Definition: pointer_expr.h:48
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
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:832
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:834
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:803
const exprt & size() const
Definition: pointer_expr.h:815
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:805
const exprt & pointer() const
Definition: pointer_expr.h:810
The reference type.
Definition: pointer_expr.h:107
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:109
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:115
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:113
An expression with three operands.
Definition: std_expr.h:49
exprt & op1()
Definition: expr.h:128
exprt & op2()
Definition: expr.h:131
exprt & op0()
Definition: expr.h:125
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:184
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:50
Generic base class for unary expressions.
Definition: std_expr.h:314
const exprt & op() const
Definition: std_expr.h:326
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:528
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:850
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:852
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:226
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:135
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:594
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:96
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:821
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:858
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
Definition: pointer_expr.h:925
const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)
Cast an exprt to a is_cstring_exprt.
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.
Definition: pointer_expr.h:985
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:143
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:285
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:610
bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)
Definition: pointer_expr.h:393
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:757
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:773
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:150
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:340
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)
bool can_cast_expr< object_address_exprt >(const exprt &base)
Definition: pointer_expr.h:510
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:79
bool can_cast_expr< is_cstring_exprt >(const exprt &base)
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
Definition: pointer_expr.h:907
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:444
bool can_cast_expr< pointer_offset_exprt >(const exprt &base)
Definition: pointer_expr.h:966
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:148
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:238
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:351
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:681
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
Definition: pointer_expr.h:403
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:526
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:221
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:301
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:460
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:840
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:697
bool can_cast_expr< writeable_object_exprt >(const exprt &base)
bool can_cast_expr< pointer_object_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:510
#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