cprover
std_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pre-defined types
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_STD_TYPES_H
14 #define CPROVER_UTIL_STD_TYPES_H
15 
16 #include "expr.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "mp_arith.h"
20 #include "validate.h"
21 #include <util/narrow.h>
22 
23 #include <unordered_map>
24 
25 class constant_exprt;
26 class namespacet;
27 
30 inline bool is_constant(const typet &type)
31 {
32  return type.get_bool(ID_C_constant);
33 }
34 
36 class bool_typet:public typet
37 {
38 public:
39  bool_typet():typet(ID_bool)
40  {
41  }
42 };
43 
45 class empty_typet:public typet
46 {
47 public:
48  empty_typet():typet(ID_empty)
49  {
50  }
51 };
52 
57 {
58 public:
59  explicit struct_union_typet(const irep_idt &_id):typet(_id)
60  {
61  }
62 
63  class componentt:public exprt
64  {
65  public:
66  componentt() = default;
67 
68  componentt(const irep_idt &_name, typet _type)
69  {
70  set_name(_name);
71  type().swap(_type);
72  }
73 
74  const irep_idt &get_name() const
75  {
76  return get(ID_name);
77  }
78 
79  void set_name(const irep_idt &name)
80  {
81  return set(ID_name, name);
82  }
83 
84  const irep_idt &get_base_name() const
85  {
86  return get(ID_base_name);
87  }
88 
89  void set_base_name(const irep_idt &base_name)
90  {
91  return set(ID_base_name, base_name);
92  }
93 
94  const irep_idt &get_access() const
95  {
96  return get(ID_access);
97  }
98 
99  void set_access(const irep_idt &access)
100  {
101  return set(ID_access, access);
102  }
103 
104  const irep_idt &get_pretty_name() const
105  {
106  return get(ID_pretty_name);
107  }
108 
109  void set_pretty_name(const irep_idt &name)
110  {
111  return set(ID_pretty_name, name);
112  }
113 
114  bool get_anonymous() const
115  {
116  return get_bool(ID_anonymous);
117  }
118 
119  void set_anonymous(bool anonymous)
120  {
121  return set(ID_anonymous, anonymous);
122  }
123 
124  bool get_is_padding() const
125  {
126  return get_bool(ID_C_is_padding);
127  }
128 
129  void set_is_padding(bool is_padding)
130  {
131  return set(ID_C_is_padding, is_padding);
132  }
133  };
134 
135  typedef std::vector<componentt> componentst;
136 
137  struct_union_typet(const irep_idt &_id, componentst _components) : typet(_id)
138  {
139  components() = std::move(_components);
140  }
141 
142  const componentst &components() const
143  {
144  return (const componentst &)(find(ID_components).get_sub());
145  }
146 
148  {
149  return (componentst &)(add(ID_components).get_sub());
150  }
151 
152  bool has_component(const irep_idt &component_name) const
153  {
154  return get_component(component_name).is_not_nil();
155  }
156 
157  const componentt &get_component(
158  const irep_idt &component_name) const;
159 
160  std::size_t component_number(const irep_idt &component_name) const;
161  const typet &component_type(const irep_idt &component_name) const;
162 
163  irep_idt get_tag() const { return get(ID_tag); }
164  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
165 
167  bool is_class() const
168  {
169  return id() == ID_struct && get_bool(ID_C_class);
170  }
171 
175  {
176  return is_class() ? ID_private : ID_public;
177  }
178 
180  bool is_incomplete() const
181  {
182  return get_bool(ID_incomplete);
183  }
184 
187  {
188  set(ID_incomplete, true);
189  }
190 };
191 
195 template <>
196 inline bool can_cast_type<struct_union_typet>(const typet &type)
197 {
198  return type.id() == ID_struct || type.id() == ID_union;
199 }
200 
210 {
212  return static_cast<const struct_union_typet &>(type);
213 }
214 
217 {
219  return static_cast<struct_union_typet &>(type);
220 }
221 
222 class struct_tag_typet;
223 
226 {
227 public:
229  {
230  }
231 
232  explicit struct_typet(componentst _components)
233  : struct_union_typet(ID_struct, std::move(_components))
234  {
235  }
236 
237  bool is_prefix_of(const struct_typet &other) const;
238 
240  bool is_class() const
241  {
242  return get_bool(ID_C_class);
243  }
244 
246  class baset : public exprt
247  {
248  public:
250  const struct_tag_typet &type() const;
251  explicit baset(struct_tag_typet base);
252  };
253 
254  typedef std::vector<baset> basest;
255 
257  const basest &bases() const
258  {
259  return (const basest &)find(ID_bases).get_sub();
260  }
261 
264  {
265  return (basest &)add(ID_bases).get_sub();
266  }
267 
270  void add_base(const struct_tag_typet &base);
271 
275  optionalt<baset> get_base(const irep_idt &id) const;
276 
280  bool has_base(const irep_idt &id) const
281  {
282  return get_base(id).has_value();
283  }
284 };
285 
289 template <>
290 inline bool can_cast_type<struct_typet>(const typet &type)
291 {
292  return type.id() == ID_struct;
293 }
294 
303 inline const struct_typet &to_struct_type(const typet &type)
304 {
306  return static_cast<const struct_typet &>(type);
307 }
308 
311 {
313  return static_cast<struct_typet &>(type);
314 }
315 
320 {
321 public:
323  {
324  set(ID_C_class, true);
325  }
326 
329 
330  const methodst &methods() const
331  {
332  return (const methodst &)(find(ID_methods).get_sub());
333  }
334 
336  {
337  return (methodst &)(add(ID_methods).get_sub());
338  }
339 
342 
344  {
345  return (const static_memberst &)(find(ID_static_members).get_sub());
346  }
347 
349  {
350  return (static_memberst &)(add(ID_static_members).get_sub());
351  }
352 
353  bool is_abstract() const
354  {
355  return get_bool(ID_abstract);
356  }
357 };
358 
362 template <>
363 inline bool can_cast_type<class_typet>(const typet &type)
364 {
365  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
366 }
367 
376 inline const class_typet &to_class_type(const typet &type)
377 {
379  return static_cast<const class_typet &>(type);
380 }
381 
384 {
386  return static_cast<class_typet &>(type);
387 }
388 
393 {
394 public:
396  {
397  }
398 
399  explicit union_typet(componentst _components)
400  : struct_union_typet(ID_union, std::move(_components))
401  {
402  }
403 };
404 
408 template <>
409 inline bool can_cast_type<union_typet>(const typet &type)
410 {
411  return type.id() == ID_union;
412 }
413 
422 inline const union_typet &to_union_type(const typet &type)
423 {
425  return static_cast<const union_typet &>(type);
426 }
427 
430 {
432  return static_cast<union_typet &>(type);
433 }
434 
436 class tag_typet:public typet
437 {
438 public:
439  explicit tag_typet(
440  const irep_idt &_id,
441  const irep_idt &identifier):typet(_id)
442  {
443  set_identifier(identifier);
444  }
445 
446  void set_identifier(const irep_idt &identifier)
447  {
448  set(ID_identifier, identifier);
449  }
450 
451  const irep_idt &get_identifier() const
452  {
453  return get(ID_identifier);
454  }
455 };
456 
460 template <>
461 inline bool can_cast_type<tag_typet>(const typet &type)
462 {
463  return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
464  type.id() == ID_union_tag;
465 }
466 
475 inline const tag_typet &to_tag_type(const typet &type)
476 {
478  return static_cast<const tag_typet &>(type);
479 }
480 
483 {
485  return static_cast<tag_typet &>(type);
486 }
487 
490 {
491 public:
492  explicit struct_tag_typet(const irep_idt &identifier):
493  tag_typet(ID_struct_tag, identifier)
494  {
495  }
496 };
497 
501 template <>
502 inline bool can_cast_type<struct_tag_typet>(const typet &type)
503 {
504  return type.id() == ID_struct_tag;
505 }
506 
515 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
516 {
518  return static_cast<const struct_tag_typet &>(type);
519 }
520 
523 {
525  return static_cast<struct_tag_typet &>(type);
526 }
527 
530 {
531 public:
532  explicit union_tag_typet(const irep_idt &identifier):
533  tag_typet(ID_union_tag, identifier)
534  {
535  }
536 };
537 
541 template <>
542 inline bool can_cast_type<union_tag_typet>(const typet &type)
543 {
544  return type.id() == ID_union_tag;
545 }
546 
555 inline const union_tag_typet &to_union_tag_type(const typet &type)
556 {
558  return static_cast<const union_tag_typet &>(type);
559 }
560 
563 {
565  return static_cast<union_tag_typet &>(type);
566 }
567 
571 {
572 public:
573  enumeration_typet():typet(ID_enumeration)
574  {
575  }
576 
577  const irept::subt &elements() const
578  {
579  return find(ID_elements).get_sub();
580  }
581 
583  {
584  return add(ID_elements).get_sub();
585  }
586 };
587 
591 template <>
592 inline bool can_cast_type<enumeration_typet>(const typet &type)
593 {
594  return type.id() == ID_enumeration;
595 }
596 
605 inline const enumeration_typet &to_enumeration_type(const typet &type)
606 {
608  return static_cast<const enumeration_typet &>(type);
609 }
610 
613 {
615  return static_cast<enumeration_typet &>(type);
616 }
617 
620 {
621 public:
622  explicit c_enum_typet(typet _subtype)
623  : type_with_subtypet(ID_c_enum, std::move(_subtype))
624  {
625  }
626 
627  class c_enum_membert:public irept
628  {
629  public:
630  irep_idt get_value() const { return get(ID_value); }
631  void set_value(const irep_idt &value) { set(ID_value, value); }
632  irep_idt get_identifier() const { return get(ID_identifier); }
633  void set_identifier(const irep_idt &identifier)
634  {
635  set(ID_identifier, identifier);
636  }
637  irep_idt get_base_name() const { return get(ID_base_name); }
638  void set_base_name(const irep_idt &base_name)
639  {
640  set(ID_base_name, base_name);
641  }
642  };
643 
644  typedef std::vector<c_enum_membert> memberst;
645 
646  const memberst &members() const
647  {
648  return (const memberst &)(find(ID_body).get_sub());
649  }
650 
652  bool is_incomplete() const
653  {
654  return get_bool(ID_incomplete);
655  }
656 
659  {
660  set(ID_incomplete, true);
661  }
662 };
663 
667 template <>
668 inline bool can_cast_type<c_enum_typet>(const typet &type)
669 {
670  return type.id() == ID_c_enum;
671 }
672 
681 inline const c_enum_typet &to_c_enum_type(const typet &type)
682 {
684  return static_cast<const c_enum_typet &>(type);
685 }
686 
689 {
691  return static_cast<c_enum_typet &>(type);
692 }
693 
696 {
697 public:
698  explicit c_enum_tag_typet(const irep_idt &identifier):
699  tag_typet(ID_c_enum_tag, identifier)
700  {
701  }
702 };
703 
707 template <>
708 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
709 {
710  return type.id() == ID_c_enum_tag;
711 }
712 
721 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
722 {
724  return static_cast<const c_enum_tag_typet &>(type);
725 }
726 
729 {
731  return static_cast<c_enum_tag_typet &>(type);
732 }
733 
735 class code_typet:public typet
736 {
737 public:
738  class parametert;
739  typedef std::vector<parametert> parameterst;
740 
744  code_typet(parameterst _parameters, typet _return_type) : typet(ID_code)
745  {
746  parameters().swap(_parameters);
747  return_type().swap(_return_type);
748  }
749 
750  // used to be argumentt -- now uses standard terminology
751 
752  class parametert:public exprt
753  {
754  public:
755  DEPRECATED(SINCE(2018, 9, 21, "use parametert(type) instead"))
756  parametert():exprt(ID_parameter)
757  {
758  }
759 
760  explicit parametert(const typet &type):exprt(ID_parameter, type)
761  {
762  }
763 
764  const exprt &default_value() const
765  {
766  return find_expr(ID_C_default_value);
767  }
768 
769  bool has_default_value() const
770  {
771  return default_value().is_not_nil();
772  }
773 
775  {
776  return add_expr(ID_C_default_value);
777  }
778 
779  // The following for methods will go away;
780  // these should not be part of the signature of a function,
781  // but rather part of the body.
782  void set_identifier(const irep_idt &identifier)
783  {
784  set(ID_C_identifier, identifier);
785  }
786 
787  void set_base_name(const irep_idt &name)
788  {
789  set(ID_C_base_name, name);
790  }
791 
792  const irep_idt &get_identifier() const
793  {
794  return get(ID_C_identifier);
795  }
796 
797  const irep_idt &get_base_name() const
798  {
799  return get(ID_C_base_name);
800  }
801 
802  bool get_this() const
803  {
804  return get_bool(ID_C_this);
805  }
806 
807  void set_this()
808  {
809  set(ID_C_this, true);
810  }
811  };
812 
813  bool has_ellipsis() const
814  {
815  return find(ID_parameters).get_bool(ID_ellipsis);
816  }
817 
818  bool has_this() const
819  {
820  return get_this() != nullptr;
821  }
822 
823  const parametert *get_this() const
824  {
825  const parameterst &p=parameters();
826  if(!p.empty() && p.front().get_this())
827  return &p.front();
828  else
829  return nullptr;
830  }
831 
832  bool is_KnR() const
833  {
834  return get_bool(ID_C_KnR);
835  }
836 
838  {
839  add(ID_parameters).set(ID_ellipsis, true);
840  }
841 
843  {
844  add(ID_parameters).remove(ID_ellipsis);
845  }
846 
847  const typet &return_type() const
848  {
849  return find_type(ID_return_type);
850  }
851 
853  {
854  return add_type(ID_return_type);
855  }
856 
857  const parameterst &parameters() const
858  {
859  return (const parameterst &)find(ID_parameters).get_sub();
860  }
861 
863  {
864  return (parameterst &)add(ID_parameters).get_sub();
865  }
866 
867  bool get_inlined() const
868  {
869  return get_bool(ID_C_inlined);
870  }
871 
872  void set_inlined(bool value)
873  {
874  set(ID_C_inlined, value);
875  }
876 
877  const irep_idt &get_access() const
878  {
879  return get(ID_access);
880  }
881 
882  void set_access(const irep_idt &access)
883  {
884  return set(ID_access, access);
885  }
886 
887  bool get_is_constructor() const
888  {
889  return get_bool(ID_constructor);
890  }
891 
893  {
894  set(ID_constructor, true);
895  }
896 
898  std::vector<irep_idt> parameter_identifiers() const
899  {
900  std::vector<irep_idt> result;
901  const parameterst &p=parameters();
902  result.reserve(p.size());
903  for(parameterst::const_iterator it=p.begin();
904  it!=p.end(); it++)
905  result.push_back(it->get_identifier());
906  return result;
907  }
908 
909  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
910 
913  {
915  const parameterst &params = parameters();
916  parameter_indices.reserve(params.size());
917  std::size_t index = 0;
918  for(const auto &p : params)
919  {
920  const irep_idt &id = p.get_identifier();
921  if(!id.empty())
922  parameter_indices.insert({ id, index });
923  ++index;
924  }
925  return parameter_indices;
926  }
927 };
928 
932 template <>
933 inline bool can_cast_type<code_typet>(const typet &type)
934 {
935  return type.id() == ID_code;
936 }
937 
946 inline const code_typet &to_code_type(const typet &type)
947 {
949  code_typet::check(type);
950  return static_cast<const code_typet &>(type);
951 }
952 
955 {
957  code_typet::check(type);
958  return static_cast<code_typet &>(type);
959 }
960 
965 {
966 public:
967  array_typet(typet _subtype, exprt _size)
968  : type_with_subtypet(ID_array, std::move(_subtype))
969  {
970  add(ID_size, std::move(_size));
971  }
972 
973  const exprt &size() const
974  {
975  return static_cast<const exprt &>(find(ID_size));
976  }
977 
979  {
980  return static_cast<exprt &>(add(ID_size));
981  }
982 
983  bool is_complete() const
984  {
985  return size().is_not_nil();
986  }
987 
988  bool is_incomplete() const
989  {
990  return size().is_nil();
991  }
992 };
993 
997 template <>
998 inline bool can_cast_type<array_typet>(const typet &type)
999 {
1000  return type.id() == ID_array;
1001 }
1002 
1011 inline const array_typet &to_array_type(const typet &type)
1012 {
1014  return static_cast<const array_typet &>(type);
1015 }
1016 
1019 {
1021  return static_cast<array_typet &>(type);
1022 }
1023 
1029 class bitvector_typet : public typet
1030 {
1031 public:
1032  explicit bitvector_typet(const irep_idt &_id) : typet(_id)
1033  {
1034  }
1035 
1036  bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
1037  {
1038  set_width(width);
1039  }
1040 
1041  std::size_t get_width() const
1042  {
1043  return get_size_t(ID_width);
1044  }
1045 
1046  void set_width(std::size_t width)
1047  {
1048  set(ID_width, narrow_cast<long long>(width));
1049  }
1050 
1051  static void check(
1052  const typet &type,
1054  {
1055  DATA_CHECK(
1056  vm, !type.get(ID_width).empty(), "bitvector type must have width");
1057  }
1058 };
1059 
1063 template <>
1064 inline bool can_cast_type<bitvector_typet>(const typet &type)
1065 {
1066  return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
1067  type.id() == ID_fixedbv || type.id() == ID_floatbv ||
1068  type.id() == ID_verilog_signedbv ||
1069  type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
1070  type.id() == ID_pointer || type.id() == ID_c_bit_field ||
1071  type.id() == ID_c_bool;
1072 }
1073 
1076 inline bool is_signed_or_unsigned_bitvector(const typet &type)
1077 {
1078  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
1079 }
1080 
1089 inline const bitvector_typet &to_bitvector_type(const typet &type)
1090 {
1092 
1093  return static_cast<const bitvector_typet &>(type);
1094 }
1095 
1098 {
1100 
1101  return static_cast<bitvector_typet &>(type);
1102 }
1103 
1106 {
1107 public:
1108  explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
1109  {
1110  set_width(width);
1111  }
1112 
1113  static void check(
1114  const typet &type,
1116  {
1117  DATA_CHECK(
1118  vm, !type.get(ID_width).empty(), "bitvector type must have width");
1119  }
1120 };
1121 
1125 template <>
1126 inline bool can_cast_type<bv_typet>(const typet &type)
1127 {
1128  return type.id() == ID_bv;
1129 }
1130 
1139 inline const bv_typet &to_bv_type(const typet &type)
1140 {
1142  bv_typet::check(type);
1143  return static_cast<const bv_typet &>(type);
1144 }
1145 
1147 inline bv_typet &to_bv_type(typet &type)
1148 {
1150  bv_typet::check(type);
1151  return static_cast<bv_typet &>(type);
1152 }
1153 
1156 {
1157 public:
1158  integer_bitvector_typet(const irep_idt &id, std::size_t width)
1159  : bitvector_typet(id, width)
1160  {
1161  }
1162 
1164  mp_integer smallest() const;
1166  mp_integer largest() const;
1167 
1168  // If we ever need any of the following three methods in \ref fixedbv_typet or
1169  // \ref floatbv_typet, we might want to move them to a new class
1170  // numeric_bitvector_typet, which would be between integer_bitvector_typet and
1171  // bitvector_typet in the hierarchy.
1172 
1174  constant_exprt smallest_expr() const;
1176  constant_exprt zero_expr() const;
1178  constant_exprt largest_expr() const;
1179 };
1180 
1184 template <>
1186 {
1187  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
1188 }
1189 
1198 inline const integer_bitvector_typet &
1200 {
1202 
1203  return static_cast<const integer_bitvector_typet &>(type);
1204 }
1205 
1208 {
1210 
1211  return static_cast<integer_bitvector_typet &>(type);
1212 }
1213 
1216 {
1217 public:
1218  explicit unsignedbv_typet(std::size_t width)
1219  : integer_bitvector_typet(ID_unsignedbv, width)
1220  {
1221  }
1222 
1223  static void check(
1224  const typet &type,
1226  {
1227  bitvector_typet::check(type, vm);
1228  }
1229 };
1230 
1234 template <>
1235 inline bool can_cast_type<unsignedbv_typet>(const typet &type)
1236 {
1237  return type.id() == ID_unsignedbv;
1238 }
1239 
1248 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
1249 {
1252  return static_cast<const unsignedbv_typet &>(type);
1253 }
1254 
1257 {
1260  return static_cast<unsignedbv_typet &>(type);
1261 }
1262 
1265 {
1266 public:
1267  explicit signedbv_typet(std::size_t width)
1268  : integer_bitvector_typet(ID_signedbv, width)
1269  {
1270  }
1271 
1272  static void check(
1273  const typet &type,
1275  {
1276  DATA_CHECK(
1277  vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
1278  }
1279 };
1280 
1284 template <>
1285 inline bool can_cast_type<signedbv_typet>(const typet &type)
1286 {
1287  return type.id() == ID_signedbv;
1288 }
1289 
1298 inline const signedbv_typet &to_signedbv_type(const typet &type)
1299 {
1301  signedbv_typet::check(type);
1302  return static_cast<const signedbv_typet &>(type);
1303 }
1304 
1307 {
1309  signedbv_typet::check(type);
1310  return static_cast<signedbv_typet &>(type);
1311 }
1312 
1318 {
1319 public:
1321  {
1322  }
1323 
1324  std::size_t get_fraction_bits() const
1325  {
1326  return get_width()-get_integer_bits();
1327  }
1328 
1329  std::size_t get_integer_bits() const;
1330 
1331  void set_integer_bits(std::size_t b)
1332  {
1333  set(ID_integer_bits, narrow_cast<long long>(b));
1334  }
1335 
1336  static void check(
1337  const typet &type,
1339  {
1340  DATA_CHECK(
1341  vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
1342  }
1343 };
1344 
1348 template <>
1349 inline bool can_cast_type<fixedbv_typet>(const typet &type)
1350 {
1351  return type.id() == ID_fixedbv;
1352 }
1353 
1362 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
1363 {
1365  fixedbv_typet::check(type);
1366  return static_cast<const fixedbv_typet &>(type);
1367 }
1368 
1371 {
1373  fixedbv_typet::check(type);
1374  return static_cast<fixedbv_typet &>(type);
1375 }
1376 
1379 {
1380 public:
1382  {
1383  }
1384 
1385  std::size_t get_e() const
1386  {
1387  // subtract one for sign bit
1388  return get_width()-get_f()-1;
1389  }
1390 
1391  std::size_t get_f() const;
1392 
1393  void set_f(std::size_t b)
1394  {
1395  set(ID_f, narrow_cast<long long>(b));
1396  }
1397 
1398  static void check(
1399  const typet &type,
1401  {
1402  DATA_CHECK(
1403  vm, !type.get(ID_width).empty(), "float bitvector type must have width");
1404  }
1405 };
1406 
1410 template <>
1411 inline bool can_cast_type<floatbv_typet>(const typet &type)
1412 {
1413  return type.id() == ID_floatbv;
1414 }
1415 
1424 inline const floatbv_typet &to_floatbv_type(const typet &type)
1425 {
1427  floatbv_typet::check(type);
1428  return static_cast<const floatbv_typet &>(type);
1429 }
1430 
1433 {
1435  floatbv_typet::check(type);
1436  return static_cast<floatbv_typet &>(type);
1437 }
1438 
1443 {
1444 public:
1445  explicit c_bit_field_typet(typet _subtype, std::size_t width)
1446  : bitvector_typet(ID_c_bit_field, width)
1447  {
1448  subtype().swap(_subtype);
1449  }
1450 
1451  // These have a sub-type
1452 };
1453 
1457 template <>
1458 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
1459 {
1460  return type.id() == ID_c_bit_field;
1461 }
1462 
1471 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
1472 {
1474  return static_cast<const c_bit_field_typet &>(type);
1475 }
1476 
1479 {
1481  return static_cast<c_bit_field_typet &>(type);
1482 }
1483 
1488 {
1489 public:
1490  pointer_typet(typet _subtype, std::size_t width)
1491  : bitvector_typet(ID_pointer, width)
1492  {
1493  subtype().swap(_subtype);
1494  }
1495 
1497  {
1498  return signedbv_typet(get_width());
1499  }
1500 
1501  static void check(
1502  const typet &type,
1504  {
1505  DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
1506  }
1507 };
1508 
1512 template <>
1513 inline bool can_cast_type<pointer_typet>(const typet &type)
1514 {
1515  return type.id() == ID_pointer;
1516 }
1517 
1526 inline const pointer_typet &to_pointer_type(const typet &type)
1527 {
1529  pointer_typet::check(type);
1530  return static_cast<const pointer_typet &>(type);
1531 }
1532 
1535 {
1537  pointer_typet::check(type);
1538  return static_cast<pointer_typet &>(type);
1539 }
1540 
1543 inline bool is_void_pointer(const typet &type)
1544 {
1545  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
1546 }
1547 
1553 {
1554 public:
1555  reference_typet(typet _subtype, std::size_t _width)
1556  : pointer_typet(std::move(_subtype), _width)
1557  {
1558  set(ID_C_reference, true);
1559  }
1560 };
1561 
1565 template <>
1566 inline bool can_cast_type<reference_typet>(const typet &type)
1567 {
1568  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
1569 }
1570 
1571 inline void validate_type(const reference_typet &type)
1572 {
1573  DATA_INVARIANT(!type.get(ID_width).empty(), "reference must have width");
1574  DATA_INVARIANT(type.get_width() > 0, "reference must have non-zero width");
1575 }
1576 
1585 inline const reference_typet &to_reference_type(const typet &type)
1586 {
1588  return static_cast<const reference_typet &>(type);
1589 }
1590 
1593 {
1595  return static_cast<reference_typet &>(type);
1596 }
1597 
1598 bool is_reference(const typet &type);
1599 
1600 bool is_rvalue_reference(const typet &type);
1601 
1604 {
1605 public:
1606  explicit c_bool_typet(std::size_t width):
1607  bitvector_typet(ID_c_bool, width)
1608  {
1609  }
1610 
1611  static void check(
1612  const typet &type,
1614  {
1615  DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
1616  }
1617 };
1618 
1622 template <>
1623 inline bool can_cast_type<c_bool_typet>(const typet &type)
1624 {
1625  return type.id() == ID_c_bool;
1626 }
1627 
1636 inline const c_bool_typet &to_c_bool_type(const typet &type)
1637 {
1639  c_bool_typet::check(type);
1640  return static_cast<const c_bool_typet &>(type);
1641 }
1642 
1645 {
1647  c_bool_typet::check(type);
1648  return static_cast<c_bool_typet &>(type);
1649 }
1650 
1654 class string_typet:public typet
1655 {
1656 public:
1657  string_typet():typet(ID_string)
1658  {
1659  }
1660 };
1661 
1665 template <>
1666 inline bool can_cast_type<string_typet>(const typet &type)
1667 {
1668  return type.id() == ID_string;
1669 }
1670 
1679 inline const string_typet &to_string_type(const typet &type)
1680 {
1682  return static_cast<const string_typet &>(type);
1683 }
1684 
1687 {
1689  return static_cast<string_typet &>(type);
1690 }
1691 
1693 class range_typet:public typet
1694 {
1695 public:
1696  range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
1697  {
1698  set_from(_from);
1699  set_to(_to);
1700  }
1701 
1702  mp_integer get_from() const;
1703  mp_integer get_to() const;
1704 
1705  void set_from(const mp_integer &_from);
1706  void set_to(const mp_integer &to);
1707 };
1708 
1712 template <>
1713 inline bool can_cast_type<range_typet>(const typet &type)
1714 {
1715  return type.id() == ID_range;
1716 }
1717 
1726 inline const range_typet &to_range_type(const typet &type)
1727 {
1729  return static_cast<const range_typet &>(type);
1730 }
1731 
1734 {
1736  return static_cast<range_typet &>(type);
1737 }
1738 
1750 {
1751 public:
1752  vector_typet(const typet &_subtype, const constant_exprt &_size);
1753 
1754  const constant_exprt &size() const;
1755  constant_exprt &size();
1756 };
1757 
1761 template <>
1762 inline bool can_cast_type<vector_typet>(const typet &type)
1763 {
1764  return type.id() == ID_vector;
1765 }
1766 
1775 inline const vector_typet &to_vector_type(const typet &type)
1776 {
1778  return static_cast<const vector_typet &>(type);
1779 }
1780 
1783 {
1785  return static_cast<vector_typet &>(type);
1786 }
1787 
1790 {
1791 public:
1792  explicit complex_typet(typet _subtype)
1793  : type_with_subtypet(ID_complex, std::move(_subtype))
1794  {
1795  }
1796 };
1797 
1801 template <>
1802 inline bool can_cast_type<complex_typet>(const typet &type)
1803 {
1804  return type.id() == ID_complex;
1805 }
1806 
1815 inline const complex_typet &to_complex_type(const typet &type)
1816 {
1818  return static_cast<const complex_typet &>(type);
1819 }
1820 
1823 {
1825  return static_cast<complex_typet &>(type);
1826 }
1827 
1829  const typet &type,
1830  const namespacet &ns);
1831 
1832 #endif // CPROVER_UTIL_STD_TYPES_H
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1636
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
floatbv_typet::set_f
void set_f(std::size_t b)
Definition: std_types.h:1393
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:813
to_enumeration_type
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:605
struct_tag_typet::struct_tag_typet
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:492
tag_typet::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:446
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
struct_typet::get_base
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:93
class_typet::methodst
componentst methodst
Definition: std_types.h:328
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:619
array_typet::is_incomplete
bool is_incomplete() const
Definition: std_types.h:988
exprt::find_expr
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:330
class_typet
Class type.
Definition: std_types.h:319
c_enum_typet::c_enum_typet
c_enum_typet(typet _subtype)
Definition: std_types.h:622
can_cast_type< unsignedbv_typet >
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Definition: std_types.h:1235
c_enum_typet::c_enum_membert::set_value
void set_value(const irep_idt &value)
Definition: std_types.h:631
struct_union_typet::componentt::get_anonymous
bool get_anonymous() const
Definition: std_types.h:114
struct_union_typet::componentt::componentt
componentt(const irep_idt &_name, typet _type)
Definition: std_types.h:68
c_enum_typet::is_incomplete
bool is_incomplete() const
enum types may be incomplete
Definition: std_types.h:652
fixedbv_typet::set_integer_bits
void set_integer_bits(std::size_t b)
Definition: std_types.h:1331
mp_arith.h
struct_union_typet::componentt::componentt
componentt()=default
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
code_typet::parametert::default_value
exprt & default_value()
Definition: std_types.h:774
integer_bitvector_typet::smallest
mp_integer smallest() const
Return the smallest value that can be represented using this type.
Definition: std_types.cpp:166
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
struct_union_typet::componentt::set_access
void set_access(const irep_idt &access)
Definition: std_types.h:99
enumeration_typet
An enumeration type, i.e., a type with elements (not to be confused with C enums)
Definition: std_types.h:570
struct_union_typet::componentt::set_anonymous
void set_anonymous(bool anonymous)
Definition: std_types.h:119
class_typet::is_abstract
bool is_abstract() const
Definition: std_types.h:353
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
can_cast_type< c_enum_tag_typet >
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
Definition: std_types.h:708
reference_typet
The reference type.
Definition: std_types.h:1552
array_typet::is_complete
bool is_complete() const
Definition: std_types.h:983
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
integer_bitvector_typet::largest_expr
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
Definition: std_types.cpp:186
typet
The type of an expression, extends irept.
Definition: type.h:28
can_cast_type< reference_typet >
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: std_types.h:1566
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
c_bit_field_typet::c_bit_field_typet
c_bit_field_typet(typet _subtype, std::size_t width)
Definition: std_types.h:1445
tag_typet::tag_typet
tag_typet(const irep_idt &_id, const irep_idt &identifier)
Definition: std_types.h:439
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:376
c_bool_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1611
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
floatbv_typet::get_f
std::size_t get_f() const
Definition: std_types.cpp:28
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:782
can_cast_type< bv_typet >
bool can_cast_type< bv_typet >(const typet &type)
Check whether a reference to a typet is a bv_typet.
Definition: std_types.h:1126
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:644
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
class_typet::static_members
static_memberst & static_members()
Definition: std_types.h:348
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1378
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
struct_typet::has_base
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
Definition: std_types.h:280
struct_typet::baset::baset
baset(struct_tag_typet base)
Definition: std_types.cpp:83
can_cast_type< union_typet >
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
Definition: std_types.h:409
empty_typet::empty_typet
empty_typet()
Definition: std_types.h:48
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
invariant.h
is_signed_or_unsigned_bitvector
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
Definition: std_types.h:1076
struct_typet::is_prefix_of
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
Definition: std_types.cpp:107
can_cast_type< complex_typet >
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
Definition: std_types.h:1802
unsignedbv_typet::unsignedbv_typet
unsignedbv_typet(std::size_t width)
Definition: std_types.h:1218
can_cast_type< c_bool_typet >
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
Definition: std_types.h:1623
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
exprt
Base class for all expressions.
Definition: expr.h:52
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
struct_union_typet::componentt::get_access
const irep_idt & get_access() const
Definition: std_types.h:94
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:489
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1789
c_enum_typet::make_incomplete
void make_incomplete()
enum types may be incomplete
Definition: std_types.h:658
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: std_types.h:1585
vector_typet
The vector type.
Definition: std_types.h:1749
struct_union_typet::componentt::get_pretty_name
const irep_idt & get_pretty_name() const
Definition: std_types.h:104
bool_typet
The Boolean type.
Definition: std_types.h:36
struct_union_typet::make_incomplete
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:186
struct_union_typet::default_access
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition: std_types.h:174
type_with_subtypet
Type with a single subtype.
Definition: type.h:145
code_typet::parameter_indicest
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition: std_types.h:909
c_enum_typet::c_enum_membert::get_base_name
irep_idt get_base_name() const
Definition: std_types.h:637
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
bv_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1113
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
can_cast_type< enumeration_typet >
bool can_cast_type< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
Definition: std_types.h:592
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
code_typet::remove_ellipsis
void remove_ellipsis()
Definition: std_types.h:842
struct_union_typet::componentt::set_name
void set_name(const irep_idt &name)
Definition: std_types.h:79
integer_bitvector_typet::zero_expr
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
Definition: std_types.cpp:176
integer_bitvector_typet::smallest_expr
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
Definition: std_types.cpp:181
code_typet::get_is_constructor
bool get_is_constructor() const
Definition: std_types.h:887
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:529
code_typet::get_this
const parametert * get_this() const
Definition: std_types.h:823
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1215
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1139
struct_union_typet::components
componentst & components()
Definition: std_types.h:147
expr.h
narrow.h
union_typet::union_typet
union_typet(componentst _components)
Definition: std_types.h:399
array_typet::size
const exprt & size() const
Definition: std_types.h:973
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1603
string_typet::string_typet
string_typet()
Definition: std_types.h:1657
struct_union_typet::struct_union_typet
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
can_cast_type< integer_bitvector_typet >
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
Definition: std_types.h:1185
struct_union_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:167
can_cast_type< struct_typet >
bool can_cast_type< struct_typet >(const typet &type)
Check whether a reference to a typet is a struct_typet.
Definition: std_types.h:290
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
can_cast_type< vector_typet >
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition: std_types.h:1762
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
struct_union_typet::struct_union_typet
struct_union_typet(const irep_idt &_id, componentst _components)
Definition: std_types.h:137
class_typet::static_memberst
componentst static_memberst
Definition: std_types.h:341
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:797
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
empty_typet
The empty type.
Definition: std_types.h:45
code_typet::get_access
const irep_idt & get_access() const
Definition: std_types.h:877
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
bitvector_typet::bitvector_typet
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:1036
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
c_bit_field_typet
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: std_types.h:1442
code_typet::parameter_identifiers
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition: std_types.h:898
can_cast_type< fixedbv_typet >
bool can_cast_type< fixedbv_typet >(const typet &type)
Check whether a reference to a typet is a fixedbv_typet.
Definition: std_types.h:1349
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:74
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
can_cast_type< c_bit_field_typet >
bool can_cast_type< c_bit_field_typet >(const typet &type)
Check whether a reference to a typet is a c_bit_field_typet.
Definition: std_types.h:1458
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
signedbv_typet::signedbv_typet
signedbv_typet(std::size_t width)
Definition: std_types.h:1267
code_typet::set_is_constructor
void set_is_constructor()
Definition: std_types.h:892
code_typet::parametert::default_value
const exprt & default_value() const
Definition: std_types.h:764
is_void_pointer
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: std_types.h:1543
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:156
struct_typet::struct_typet
struct_typet(componentst _components)
Definition: std_types.h:232
complex_typet::complex_typet
complex_typet(typet _subtype)
Definition: std_types.h:1792
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_typet::pointer_typet
pointer_typet(typet _subtype, std::size_t width)
Definition: std_types.h:1490
struct_union_typet::componentt::get_is_padding
bool get_is_padding() const
Definition: std_types.h:124
struct_union_typet::componentt::set_pretty_name
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:109
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1264
integer_bitvector_typet::integer_bitvector_typet
integer_bitvector_typet(const irep_idt &id, std::size_t width)
Definition: std_types.h:1158
can_cast_type< array_typet >
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition: std_types.h:998
code_typet::code_typet
code_typet(parameterst _parameters, typet _return_type)
Constructs a new code type, i.e., function type.
Definition: std_types.h:744
struct_union_typet::componentt::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:89
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1471
range_typet
A type for subranges of integers.
Definition: std_types.h:1693
code_typet::set_inlined
void set_inlined(bool value)
Definition: std_types.h:872
class_typet::static_members
const static_memberst & static_members() const
Definition: std_types.h:343
struct_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:240
integer_bitvector_typet
Fixed-width bit-vector representing a signed or unsigned integer.
Definition: std_types.h:1155
c_bool_typet::c_bool_typet
c_bool_typet(std::size_t width)
Definition: std_types.h:1606
floatbv_typet::get_e
std::size_t get_e() const
Definition: std_types.h:1385
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
c_enum_typet::c_enum_membert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:633
validate_type
void validate_type(const reference_typet &type)
Definition: std_types.h:1571
bitvector_typet::bitvector_typet
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:1032
is_rvalue_reference
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:140
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: std_types.h:1199
irept::swap
void swap(irept &irep)
Definition: irep.h:463
fixedbv_typet::fixedbv_typet
fixedbv_typet()
Definition: std_types.h:1320
code_typet
Base type of functions.
Definition: std_types.h:735
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
range_typet::get_to
mp_integer get_to() const
Definition: std_types.cpp:161
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
struct_typet::basest
std::vector< baset > basest
Definition: std_types.h:254
can_cast_type< union_tag_typet >
bool can_cast_type< union_tag_typet >(const typet &type)
Check whether a reference to a typet is a union_tag_typet.
Definition: std_types.h:542
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
array_typet::size
exprt & size()
Definition: std_types.h:978
dstringt::empty
bool empty() const
Definition: dstring.h:88
union_typet
The union type.
Definition: std_types.h:392
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:436
enumeration_typet::enumeration_typet
enumeration_typet()
Definition: std_types.h:573
bitvector_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1051
reference_typet::reference_typet
reference_typet(typet _subtype, std::size_t _width)
Definition: std_types.h:1555
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
typet::check
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:100
class_typet::methodt
componentt methodt
Definition: std_types.h:327
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
can_cast_type< string_typet >
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
Definition: std_types.h:1666
code_typet::parametert::get_this
bool get_this() const
Definition: std_types.h:802
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:1046
struct_union_typet::componentt::set_is_padding
void set_is_padding(bool is_padding)
Definition: std_types.h:129
c_enum_typet::c_enum_membert::get_value
irep_idt get_value() const
Definition: std_types.h:630
struct_typet::bases
basest & bases()
Get the collection of base classes/structs.
Definition: std_types.h:263
code_typet::has_this
bool has_this() const
Definition: std_types.h:818
range_typet::range_typet
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:1696
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:787
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:807
to_range_type
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1726
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1317
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
is_constant_or_has_constant_components
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
Definition: std_types.cpp:200
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
unsignedbv_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1223
floatbv_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1398
struct_union_typet::componentt
Definition: std_types.h:63
to_string_type
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition: std_types.h:1679
c_enum_tag_typet::c_enum_tag_typet
c_enum_tag_typet(const irep_idt &identifier)
Definition: std_types.h:698
enumeration_typet::elements
const irept::subt & elements() const
Definition: std_types.h:577
floatbv_typet::floatbv_typet
floatbv_typet()
Definition: std_types.h:1381
vector_typet::vector_typet
vector_typet(const typet &_subtype, const constant_exprt &_size)
Definition: std_types.cpp:262
range_typet::set_to
void set_to(const mp_integer &to)
Definition: std_types.cpp:151
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
struct_typet::struct_typet
struct_typet()
Definition: std_types.h:228
class_typet::methods
const methodst & methods() const
Definition: std_types.h:330
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:695
array_typet
Arrays with given size.
Definition: std_types.h:964
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
c_enum_typet::c_enum_membert
Definition: std_types.h:627
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: std_types.h:1324
exprt::add_expr
exprt & add_expr(const irep_idt &name)
Definition: expr.h:325
c_enum_typet::c_enum_membert::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:638
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1029
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:837
code_typet::parametert::parametert
parametert(const typet &type)
Definition: std_types.h:760
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
fixedbv_typet::get_integer_bits
std::size_t get_integer_bits() const
Definition: std_types.cpp:21
can_cast_type< range_typet >
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition: std_types.h:1713
string_typet
String type.
Definition: std_types.h:1654
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:792
signedbv_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1272
irept::get_sub
subt & get_sub()
Definition: irep.h:477
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
can_cast_type< c_enum_typet >
bool can_cast_type< c_enum_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_typet.
Definition: std_types.h:668
code_typet::parametert
Definition: std_types.h:752
class_typet::class_typet
class_typet()
Definition: std_types.h:322
validate.h
code_typet::is_KnR
bool is_KnR() const
Definition: std_types.h:832
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:867
union_tag_typet::union_tag_typet
union_tag_typet(const irep_idt &identifier)
Definition: std_types.h:532
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:171
code_typet::return_type
typet & return_type()
Definition: std_types.h:852
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
array_typet::array_typet
array_typet(typet _subtype, exprt _size)
Definition: std_types.h:967
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:381
can_cast_type< signedbv_typet >
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
Definition: std_types.h:1285
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:81
c_enum_typet::c_enum_membert::get_identifier
irep_idt get_identifier() const
Definition: std_types.h:632
bool_typet::bool_typet
bool_typet()
Definition: std_types.h:39
bv_typet::bv_typet
bv_typet(std::size_t width)
Definition: std_types.h:1108
enumeration_typet::elements
irept::subt & elements()
Definition: std_types.h:582
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
code_typet::parameter_indices
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition: std_types.h:912
struct_union_typet::componentt::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:84
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1487
can_cast_type< class_typet >
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition: std_types.h:363
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
union_typet::union_typet
union_typet()
Definition: std_types.h:395
constant_exprt
A constant literal expression.
Definition: std_expr.h:3905
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
class_typet::methods
methodst & methods()
Definition: std_types.h:335
struct_union_typet::is_incomplete
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:180
can_cast_type< tag_typet >
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_typet.
Definition: std_types.h:461
can_cast_type< struct_union_typet >
bool can_cast_type< struct_union_typet >(const typet &type)
Check whether a reference to a typet is a struct_union_typet.
Definition: std_types.h:196
code_typet::set_access
void set_access(const irep_idt &access)
Definition: std_types.h:882
pointer_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1501
can_cast_type< floatbv_typet >
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
Definition: std_types.h:1411
pointer_typet::difference_type
signedbv_typet difference_type() const
Definition: std_types.h:1496
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1064
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1105
validation_modet::INVARIANT
code_typet::parameters
parameterst & parameters()
Definition: std_types.h:862
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
range_typet::set_from
void set_from(const mp_integer &_from)
Definition: std_types.cpp:146
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:646
code_typet::parametert::has_default_value
bool has_default_value() const
Definition: std_types.h:769
sharing_treet
Base class for tree-like data structures with sharing.
Definition: irep.h:178
fixedbv_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1336