CBMC
Loading...
Searching...
No Matches
pointer_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for Pointers
4
5Author: 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
18class namespacet;
19
24{
25public:
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
79template <>
80inline bool can_cast_type<pointer_typet>(const typet &type)
81{
82 return type.id() == ID_pointer;
83}
84
93inline const pointer_typet &to_pointer_type(const typet &type)
94{
97 return static_cast<const pointer_typet &>(type);
98}
99
102{
105 return static_cast<pointer_typet &>(type);
106}
107
110inline 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{
122public:
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);
135 vm, type.get_sub().size() == 1, "reference must have one type parameter");
137 static_cast<const reference_typet &>(type);
139 vm, !reference_type.get(ID_width).empty(), "reference must have width");
141 vm, reference_type.get_width() > 0, "reference must have non-zero width");
142 }
143};
144
148template <>
149inline bool can_cast_type<reference_typet>(const typet &type)
150{
152}
153
162inline 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
175bool is_reference(const typet &type);
176
177bool is_rvalue_reference(const typet &type);
178
181{
182public:
191
193 : binary_exprt(
194 std::move(_object),
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
234template <>
236{
237 return base.id() == ID_object_descriptor;
238}
239
240inline void validate_expr(const object_descriptor_exprt &value)
241{
242 validate_operands(value, 2, "Object descriptor must have two operands");
243}
244
251inline const object_descriptor_exprt &
253{
256 static_cast<const object_descriptor_exprt &>(expr);
258 return ret;
259}
260
269
272{
273public:
275 : binary_exprt(
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
298template <>
300{
301 return base.id() == ID_dynamic_object;
302}
303
304inline void validate_expr(const dynamic_object_exprt &value)
305{
306 validate_operands(value, 2, "Dynamic object must have two operands");
307}
308
316{
319 static_cast<const dynamic_object_exprt &>(expr);
321 return ret;
322}
323
326{
328 dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
330 return ret;
331}
332
335{
336public:
341
343 {
344 return op();
345 }
346
347 const exprt &address() const
348 {
349 return op();
350 }
351};
352
353template <>
355{
356 return base.id() == ID_is_dynamic_object;
357}
358
359inline void validate_expr(const is_dynamic_object_exprt &value)
360{
361 validate_operands(value, 1, "is_dynamic_object must have one operand");
362}
363
364inline const is_dynamic_object_exprt &
366{
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{
379 expr.operands().size() == 1, "is_dynamic_object must have one operand");
380 return static_cast<is_dynamic_object_exprt &>(expr);
381}
382
387{
388public:
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
421template <>
423{
424 return base.id() == ID_pointer_in_range;
425}
426
427inline 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{
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{
446 expr.operands().size() == 3, "pointer_in_range must have three operands");
447 return static_cast<pointer_in_range_exprt &>(expr);
448}
449
453{
454public:
456 exprt a,
457 exprt b,
458 exprt c,
460 exprt is_dead)
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
504template <>
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
518{
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{
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{
541public:
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
560template <>
562{
563 return base.id() == ID_address_of;
564}
565
566inline void validate_expr(const address_of_exprt &value)
567{
568 validate_operands(value, 1, "Address of must have one operand");
569}
570
577inline 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);
582 return ret;
583}
584
587{
588 PRECONDITION(expr.id() == ID_address_of);
589 address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
591 return ret;
592}
593
596{
597public:
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
624};
625
626template <>
628{
629 return base.id() == ID_object_address;
630}
631
632inline void validate_expr(const object_address_exprt &value)
633{
634 validate_operands(value, 0, "object_address must have zero operands");
635}
636
644{
647 static_cast<const object_address_exprt &>(expr);
649 return ret;
650}
651
654{
656 object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
658 return ret;
659}
660
664{
665public:
669 exprt base,
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
705 {
706 return get(ID_component_name);
707 }
708};
709
710template <>
712{
713 return expr.id() == ID_field_address;
714}
715
716inline void validate_expr(const field_address_exprt &value)
717{
718 validate_operands(value, 1, "field_address must have one operand");
719}
720
728{
730 const field_address_exprt &ret =
731 static_cast<const field_address_exprt &>(expr);
733 return ret;
734}
735
738{
740 field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
742 return ret;
743}
744
748{
749public:
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
797template <>
799{
800 return expr.id() == ID_element_address;
801}
802
803inline void validate_expr(const element_address_exprt &value)
804{
805 validate_operands(value, 2, "element_address must have two operands");
806}
807
815{
818 static_cast<const element_address_exprt &>(expr);
820 return ret;
821}
822
825{
827 element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
829 return ret;
830}
831
834{
835public:
836 // The given operand must have pointer type.
837 explicit dereference_exprt(const exprt &op)
839 {
840 }
841
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 {
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
873template <>
875{
876 return base.id() == ID_dereference;
877}
878
879inline void validate_expr(const dereference_exprt &value)
880{
881 validate_operands(value, 1, "Dereference must have one operand");
882}
883
891{
892 PRECONDITION(expr.id() == ID_dereference);
893 const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
895 return ret;
896}
897
900{
901 PRECONDITION(expr.id() == ID_dereference);
902 dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
904 return ret;
905}
906
909{
910public:
912 : constant_exprt(ID_NULL, std::move(type))
913 {
914 }
915};
916
920{
921public:
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
938template <>
939inline 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
944inline 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
949inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
950{
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);
955 return ret;
956}
957
960{
961public:
963 : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
964 {
965 }
966};
967
968template <>
969inline bool can_cast_expr<r_ok_exprt>(const exprt &base)
970{
971 return base.id() == ID_r_ok;
972}
973
974inline void validate_expr(const r_ok_exprt &value)
975{
976 validate_operands(value, 2, "r_ok must have two operands");
977}
978
979inline 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);
984 return ret;
985}
986
989{
990public:
992 : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
993 {
994 }
995};
996
997template <>
998inline bool can_cast_expr<w_ok_exprt>(const exprt &base)
999{
1000 return base.id() == ID_w_ok;
1001}
1002
1003inline void validate_expr(const w_ok_exprt &value)
1004{
1005 validate_operands(value, 2, "w_ok must have two operands");
1006}
1007
1008inline 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);
1013 return ret;
1014}
1015
1019{
1020public:
1022 irep_idt id,
1023 exprt pointer,
1024 exprt size,
1026 exprt is_dead)
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
1082template <>
1084{
1085 return base.id() == ID_prophecy_r_ok || base.id() == ID_prophecy_w_ok ||
1086 base.id() == ID_prophecy_rw_ok;
1087}
1088
1090{
1091 validate_operands(value, 4, "r_or_w_ok must have four operands");
1092}
1093
1094inline const prophecy_r_or_w_ok_exprt &
1096{
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);
1102 return ret;
1103}
1104
1107{
1108public:
1110 exprt pointer,
1111 exprt size,
1113 exprt is_dead)
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
1133template <>
1135{
1136 return base.id() == ID_prophecy_r_ok;
1137}
1138
1139inline 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);
1150 return ret;
1151}
1152
1155{
1156public:
1158 exprt pointer,
1159 exprt size,
1161 exprt is_dead)
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
1181template <>
1183{
1184 return base.id() == ID_prophecy_w_ok;
1185}
1186
1187inline 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);
1198 return ret;
1199}
1200
1210{
1211public:
1213 const irep_idt &_value,
1214 const exprt &_pointer)
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
1236 {
1237 return op0();
1238 }
1239};
1240
1241template <>
1243{
1244 return base.id() == ID_annotated_pointer_constant;
1245}
1246
1248{
1250 value, 1, "Annotated pointer constant must have one operand");
1251}
1252
1261{
1264 static_cast<const annotated_pointer_constant_exprt &>(expr);
1266 return ret;
1267}
1268
1279
1282{
1283public:
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
1300template <>
1302{
1303 return base.id() == ID_pointer_offset;
1304}
1305
1306inline 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{
1323 const pointer_offset_exprt &ret =
1324 static_cast<const pointer_offset_exprt &>(expr);
1326 return ret;
1327}
1328
1331{
1333 pointer_offset_exprt &ret = static_cast<pointer_offset_exprt &>(expr);
1335 return ret;
1336}
1337
1340{
1341public:
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
1358template <>
1360{
1361 return base.id() == ID_pointer_object;
1362}
1363
1364inline 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{
1381 const pointer_object_exprt &ret =
1382 static_cast<const pointer_object_exprt &>(expr);
1384 return ret;
1385}
1386
1389{
1391 pointer_object_exprt &ret = static_cast<pointer_object_exprt &>(expr);
1393 return ret;
1394}
1395
1399{
1400public:
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
1424{
1425 PRECONDITION(expr.id() == ID_object_size);
1426 const object_size_exprt &ret = static_cast<const object_size_exprt &>(expr);
1428 return ret;
1429}
1430
1433{
1434 PRECONDITION(expr.id() == ID_object_size);
1435 object_size_exprt &ret = static_cast<object_size_exprt &>(expr);
1437 return ret;
1438}
1439
1440template <>
1442{
1443 return base.id() == ID_object_size;
1444}
1445
1446inline 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{
1459public:
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
1477template <>
1479{
1480 return base.id() == ID_is_cstring;
1481}
1482
1483inline void validate_expr(const is_cstring_exprt &value)
1484{
1485 validate_operands(value, 1, "is_cstring must have one operand");
1486}
1487
1495{
1496 PRECONDITION(expr.id() == ID_is_cstring);
1497 const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
1499 return ret;
1500}
1501
1504{
1505 PRECONDITION(expr.id() == ID_is_cstring);
1506 is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
1508 return ret;
1509}
1510
1516{
1517public:
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
1535template <>
1536inline bool can_cast_expr<cstrlen_exprt>(const exprt &base)
1537{
1538 return base.id() == ID_cstrlen;
1539}
1540
1541inline void validate_expr(const cstrlen_exprt &value)
1542{
1543 validate_operands(value, 1, "cstrlen must have one operand");
1544}
1545
1552inline 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);
1557 return ret;
1558}
1559
1562{
1563 PRECONDITION(expr.id() == ID_cstrlen);
1564 cstrlen_exprt &ret = static_cast<cstrlen_exprt &>(expr);
1566 return ret;
1567}
1568
1572{
1573public:
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
1591template <>
1593{
1594 return base.id() == ID_live_object;
1595}
1596
1597inline void validate_expr(const live_object_exprt &value)
1598{
1599 validate_operands(value, 1, "live_object must have one operand");
1600}
1601
1609{
1610 PRECONDITION(expr.id() == ID_live_object);
1611 const live_object_exprt &ret = static_cast<const live_object_exprt &>(expr);
1613 return ret;
1614}
1615
1618{
1619 PRECONDITION(expr.id() == ID_live_object);
1620 live_object_exprt &ret = static_cast<live_object_exprt &>(expr);
1622 return ret;
1623}
1624
1628{
1629public:
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
1647template <>
1649{
1650 return base.id() == ID_writeable_object;
1651}
1652
1653inline void validate_expr(const writeable_object_exprt &value)
1654{
1655 validate_operands(value, 1, "writeable_object must have one operand");
1656}
1657
1665{
1668 static_cast<const writeable_object_exprt &>(expr);
1670 return ret;
1671}
1672
1675{
1677 writeable_object_exprt &ret = static_cast<writeable_object_exprt &>(expr);
1679 return ret;
1680}
1681
1684{
1685public:
1690
1693 std::move(__op0),
1695 std::move(__op1),
1696 bool_typet())
1697 {
1698 }
1699};
1700
1701template <>
1702inline bool can_cast_expr<separate_exprt>(const exprt &base)
1703{
1704 return base.id() == ID_separate;
1705}
1706
1707inline void validate_expr(const separate_exprt &value)
1708{
1709}
1710
1717inline 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);
1722 return ret;
1723}
1724
1727{
1728 PRECONDITION(expr.id() == ID_separate);
1729 separate_exprt &ret = static_cast<separate_exprt &>(expr);
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.
const exprt & object() const
address_of_exprt(exprt op, pointer_typet _type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
const irep_idt & get_value() const
void set_value(const irep_idt &value)
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 & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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
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:3117
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
cstrlen_exprt(exprt address, typet type)
exprt & address()
const exprt & address() const
Operator to dereference a pointer.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
dereference_exprt(const exprt &op)
const exprt & pointer() const
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...
dereference_exprt(exprt op, typet type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Representation of heap-allocated objects.
unsigned int get_instance() const
void set_instance(unsigned int instance)
const exprt & valid() const
dynamic_object_exprt(typet type)
Operator to return the address of an array element relative to a base address.
const typet & element_type() const
returns the type of the array element whose address is represented
const exprt & index() const
pointer_typet & type()
const pointer_typet & type() const
const exprt & base() const
Base class for all expressions.
Definition expr.h:344
exprt & op3()
Definition expr.h:142
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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.
const typet & field_type() const
returns the type of the field whose address is represented
const exprt & base() const
const irep_idt & component_name() const
pointer_typet & type()
const typet & compound_type() const
const pointer_typet & type() const
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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
subt & get_sub()
Definition irep.h:448
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.
is_dynamic_object_exprt(const exprt &op)
const exprt & address() const
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:91
The NIL expression.
Definition std_expr.h:3208
The null pointer constant.
null_pointer_exprt(pointer_typet type)
An expression without operands.
Definition std_expr.h:22
Operator to return the address of an object.
const pointer_typet & type() const
pointer_typet & type()
symbol_exprt object_expr() const
irep_idt object_identifier() const
const typet & object_type() const
returns the type of the object whose address is represented
Split an expression into a base object and a (byte) offset.
const exprt & root_object() const
object_descriptor_exprt(exprt _object)
const exprt & offset() const
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 & object() const
Expression for finding the size (in bytes) of the object a pointer points to.
object_size_exprt(exprt pointer, typet type)
const exprt & pointer() const
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
pointer_in_range_exprt(exprt a, exprt b, exprt c)
const exprt & upper_bound() const
const exprt & lower_bound() const
const exprt & pointer() const
A numerical identifier for the object a pointer points to.
const exprt & pointer() const
pointer_object_exprt(exprt pointer, typet type)
The offset (in bytes) of a pointer relative to the object.
pointer_offset_exprt(exprt pointer, typet type)
const exprt & pointer() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
signedbv_typet difference_type() const
const typet & base_type() const
The type of the data what we point to.
typet & base_type()
The type of the data what we point to.
pointer_typet(typet _base_type, std::size_t width)
const typet & subtype() const
typet & subtype()
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
const exprt & upper_bound() const
const exprt & dead_ptr() const
const exprt & lower_bound() const
const exprt & pointer() const
const exprt & deallocated_ptr() const
exprt lower(const namespacet &ns) const
prophecy_pointer_in_range_exprt(exprt a, exprt b, exprt c, exprt is_deallocated, exprt is_dead)
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 & deallocated_ptr() const
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const exprt & dead_ptr() const
const exprt & pointer() const
prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const exprt & size() 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.
r_ok_exprt(exprt pointer, exprt size)
A base class for a predicate that indicates that an address range is ok to read or write or both.
const exprt & size() const
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const exprt & pointer() const
The reference type.
reference_typet(typet _subtype, std::size_t _width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
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 & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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.
w_ok_exprt(exprt pointer, exprt size)
A predicate that indicates that the object pointed to is writeable.
writeable_object_exprt(exprt pointer)
const exprt & pointer() const
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
STL namespace.
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
bool can_cast_expr< separate_exprt >(const exprt &base)
const separate_exprt & to_separate_expr(const exprt &expr)
Cast an exprt to a separate_exprt.
void validate_expr(const object_descriptor_exprt &value)
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
const prophecy_r_ok_exprt & to_prophecy_r_ok_expr(const exprt &expr)
bool can_cast_expr< field_address_exprt >(const exprt &expr)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const prophecy_w_ok_exprt & to_prophecy_w_ok_expr(const exprt &expr)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool can_cast_expr< prophecy_w_ok_exprt >(const exprt &base)
bool can_cast_expr< live_object_exprt >(const exprt &base)
bool is_reference(const typet &type)
Returns true if the type is a reference.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)
bool can_cast_expr< prophecy_pointer_in_range_exprt >(const exprt &base)
bool can_cast_expr< dereference_exprt >(const exprt &base)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
bool can_cast_expr< cstrlen_exprt >(const exprt &base)
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
bool can_cast_expr< object_address_exprt >(const exprt &base)
const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr(const exprt &expr)
bool can_cast_expr< object_size_exprt >(const exprt &base)
bool can_cast_expr< is_cstring_exprt >(const exprt &base)
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
bool can_cast_expr< address_of_exprt >(const exprt &base)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool can_cast_expr< pointer_offset_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool can_cast_expr< w_ok_exprt >(const exprt &base)
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
bool can_cast_expr< element_address_exprt >(const exprt &expr)
bool can_cast_expr< r_ok_exprt >(const exprt &base)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)
Cast an exprt to a is_cstring_exprt.
bool can_cast_expr< r_or_w_ok_exprt >(const exprt &base)
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
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