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 
22 #include <unordered_map>
23 
24 class constant_exprt;
25 class namespacet;
26 
28 class bool_typet:public typet
29 {
30 public:
31  bool_typet():typet(ID_bool)
32  {
33  }
34 };
35 
38 // NOLINTNEXTLINE
39 class DEPRECATED("Use `optional<typet>` instead.") nil_typet : public typet
40 {
41 public:
42  nil_typet():typet(static_cast<const typet &>(get_nil_irep()))
43  {
44  }
45 };
46 
48 class empty_typet:public typet
49 {
50 public:
51  empty_typet():typet(ID_empty)
52  {
53  }
54 };
55 
57 class void_typet:public empty_typet
58 {
59 };
60 
62 class symbol_typet:public typet
63 {
64 public:
65  explicit symbol_typet(const irep_idt &identifier) : typet(ID_symbol_type)
66  {
67  set_identifier(identifier);
68  }
69 
70  void set_identifier(const irep_idt &identifier)
71  {
72  set(ID_identifier, identifier);
73  }
74 
75  const irep_idt &get_identifier() const
76  {
77  return get(ID_identifier);
78  }
79 };
80 
84 template <>
85 inline bool can_cast_type<symbol_typet>(const typet &type)
86 {
87  return type.id() == ID_symbol_type;
88 }
89 
98 inline const symbol_typet &to_symbol_type(const typet &type)
99 {
101  return static_cast<const symbol_typet &>(type);
102 }
103 
106 {
108  return static_cast<symbol_typet &>(type);
109 }
110 
115 {
116 public:
117  explicit struct_union_typet(const irep_idt &_id):typet(_id)
118  {
119  }
120 
121  class componentt:public exprt
122  {
123  public:
124  componentt() = default;
125 
126  componentt(const irep_idt &_name, const typet &_type)
127  {
128  set_name(_name);
129  type()=_type;
130  }
131 
132  const irep_idt &get_name() const
133  {
134  return get(ID_name);
135  }
136 
137  void set_name(const irep_idt &name)
138  {
139  return set(ID_name, name);
140  }
141 
142  const irep_idt &get_base_name() const
143  {
144  return get(ID_base_name);
145  }
146 
147  void set_base_name(const irep_idt &base_name)
148  {
149  return set(ID_base_name, base_name);
150  }
151 
152  const irep_idt &get_access() const
153  {
154  return get(ID_access);
155  }
156 
157  void set_access(const irep_idt &access)
158  {
159  return set(ID_access, access);
160  }
161 
162  const irep_idt &get_pretty_name() const
163  {
164  return get(ID_pretty_name);
165  }
166 
167  void set_pretty_name(const irep_idt &name)
168  {
169  return set(ID_pretty_name, name);
170  }
171 
172  bool get_anonymous() const
173  {
174  return get_bool(ID_anonymous);
175  }
176 
177  void set_anonymous(bool anonymous)
178  {
179  return set(ID_anonymous, anonymous);
180  }
181 
182  bool get_is_padding() const
183  {
184  return get_bool(ID_C_is_padding);
185  }
186 
187  void set_is_padding(bool is_padding)
188  {
189  return set(ID_C_is_padding, is_padding);
190  }
191 
192  bool get_is_final() const
193  {
194  return get_bool(ID_final);
195  }
196 
197  void set_is_final(const bool is_final)
198  {
199  set(ID_final, is_final);
200  }
201  };
202 
203  typedef std::vector<componentt> componentst;
204 
205  const componentst &components() const
206  {
207  return (const componentst &)(find(ID_components).get_sub());
208  }
209 
211  {
212  return (componentst &)(add(ID_components).get_sub());
213  }
214 
215  bool has_component(const irep_idt &component_name) const
216  {
217  return get_component(component_name).is_not_nil();
218  }
219 
220  const componentt &get_component(
221  const irep_idt &component_name) const;
222 
223  std::size_t component_number(const irep_idt &component_name) const;
224  const typet &component_type(const irep_idt &component_name) const;
225 
226  irep_idt get_tag() const { return get(ID_tag); }
227  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
228 
230  bool is_class() const
231  {
232  return id() == ID_struct && get_bool(ID_C_class);
233  }
234 
238  {
239  return is_class() ? ID_private : ID_public;
240  }
241 };
242 
246 template <>
247 inline bool can_cast_type<struct_union_typet>(const typet &type)
248 {
249  return type.id() == ID_struct || type.id() == ID_union;
250 }
251 
261 {
263  return static_cast<const struct_union_typet &>(type);
264 }
265 
268 {
270  return static_cast<struct_union_typet &>(type);
271 }
272 
273 class struct_tag_typet;
274 
277 {
278 public:
280  {
281  }
282 
283  bool is_prefix_of(const struct_typet &other) const;
284 
286  bool is_class() const
287  {
288  return get_bool(ID_C_class);
289  }
290 
292  class baset : public exprt
293  {
294  public:
296  const struct_tag_typet &type() const;
297  explicit baset(const struct_tag_typet &base);
298  };
299 
300  typedef std::vector<baset> basest;
301 
303  const basest &bases() const
304  {
305  return (const basest &)find(ID_bases).get_sub();
306  }
307 
310  {
311  return (basest &)add(ID_bases).get_sub();
312  }
313 
316  void add_base(const struct_tag_typet &base);
317 
321  optionalt<baset> get_base(const irep_idt &id) const;
322 
326  bool has_base(const irep_idt &id) const
327  {
328  return get_base(id).has_value();
329  }
330 };
331 
335 template <>
336 inline bool can_cast_type<struct_typet>(const typet &type)
337 {
338  return type.id() == ID_struct;
339 }
340 
349 inline const struct_typet &to_struct_type(const typet &type)
350 {
352  return static_cast<const struct_typet &>(type);
353 }
354 
357 {
359  return static_cast<struct_typet &>(type);
360 }
361 
366 {
367 public:
369  {
370  set(ID_C_class, true);
371  }
372 
375 
376  const methodst &methods() const
377  {
378  return (const methodst &)(find(ID_methods).get_sub());
379  }
380 
382  {
383  return (methodst &)(add(ID_methods).get_sub());
384  }
385 
386  bool is_abstract() const
387  {
388  return get_bool(ID_abstract);
389  }
390 };
391 
395 template <>
396 inline bool can_cast_type<class_typet>(const typet &type)
397 {
398  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
399 }
400 
409 inline const class_typet &to_class_type(const typet &type)
410 {
412  return static_cast<const class_typet &>(type);
413 }
414 
417 {
419  return static_cast<class_typet &>(type);
420 }
421 
426 {
427 public:
429  {
430  }
431 };
432 
436 template <>
437 inline bool can_cast_type<union_typet>(const typet &type)
438 {
439  return type.id() == ID_union;
440 }
441 
450 inline const union_typet &to_union_type(const typet &type)
451 {
453  return static_cast<const union_typet &>(type);
454 }
455 
458 {
460  return static_cast<union_typet &>(type);
461 }
462 
464 class tag_typet:public typet
465 {
466 public:
467  explicit tag_typet(
468  const irep_idt &_id,
469  const irep_idt &identifier):typet(_id)
470  {
471  set_identifier(identifier);
472  }
473 
474  void set_identifier(const irep_idt &identifier)
475  {
476  set(ID_identifier, identifier);
477  }
478 
479  const irep_idt &get_identifier() const
480  {
481  return get(ID_identifier);
482  }
483 };
484 
488 template <>
489 inline bool can_cast_type<tag_typet>(const typet &type)
490 {
491  return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
492  type.id() == ID_union_tag;
493 }
494 
503 inline const tag_typet &to_tag_type(const typet &type)
504 {
506  return static_cast<const tag_typet &>(type);
507 }
508 
511 {
513  return static_cast<tag_typet &>(type);
514 }
515 
518 {
519 public:
520  explicit struct_tag_typet(const irep_idt &identifier):
521  tag_typet(ID_struct_tag, identifier)
522  {
523  }
524 };
525 
529 template <>
530 inline bool can_cast_type<struct_tag_typet>(const typet &type)
531 {
532  return type.id() == ID_struct_tag;
533 }
534 
543 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
544 {
546  return static_cast<const struct_tag_typet &>(type);
547 }
548 
551 {
553  return static_cast<struct_tag_typet &>(type);
554 }
555 
558 {
559 public:
560  explicit union_tag_typet(const irep_idt &identifier):
561  tag_typet(ID_union_tag, identifier)
562  {
563  }
564 };
565 
569 template <>
570 inline bool can_cast_type<union_tag_typet>(const typet &type)
571 {
572  return type.id() == ID_union_tag;
573 }
574 
583 inline const union_tag_typet &to_union_tag_type(const typet &type)
584 {
586  return static_cast<const union_tag_typet &>(type);
587 }
588 
591 {
593  return static_cast<union_tag_typet &>(type);
594 }
595 
599 {
600 public:
601  enumeration_typet():typet(ID_enumeration)
602  {
603  }
604 
605  const irept::subt &elements() const
606  {
607  return find(ID_elements).get_sub();
608  }
609 
611  {
612  return add(ID_elements).get_sub();
613  }
614 };
615 
619 template <>
620 inline bool can_cast_type<enumeration_typet>(const typet &type)
621 {
622  return type.id() == ID_enumeration;
623 }
624 
633 inline const enumeration_typet &to_enumeration_type(const typet &type)
634 {
636  return static_cast<const enumeration_typet &>(type);
637 }
638 
641 {
643  return static_cast<enumeration_typet &>(type);
644 }
645 
648 {
649 public:
650  explicit c_enum_typet(const typet &_subtype):
651  type_with_subtypet(ID_c_enum, _subtype)
652  {
653  }
654 
655  class c_enum_membert:public irept
656  {
657  public:
658  irep_idt get_value() const { return get(ID_value); }
659  void set_value(const irep_idt &value) { set(ID_value, value); }
660  irep_idt get_identifier() const { return get(ID_identifier); }
661  void set_identifier(const irep_idt &identifier)
662  {
663  set(ID_identifier, identifier);
664  }
665  irep_idt get_base_name() const { return get(ID_base_name); }
666  void set_base_name(const irep_idt &base_name)
667  {
668  set(ID_base_name, base_name);
669  }
670  };
671 
672  typedef std::vector<c_enum_membert> memberst;
673 
674  const memberst &members() const
675  {
676  return (const memberst &)(find(ID_body).get_sub());
677  }
678 };
679 
683 template <>
684 inline bool can_cast_type<c_enum_typet>(const typet &type)
685 {
686  return type.id() == ID_c_enum;
687 }
688 
697 inline const c_enum_typet &to_c_enum_type(const typet &type)
698 {
700  return static_cast<const c_enum_typet &>(type);
701 }
702 
705 {
707  return static_cast<c_enum_typet &>(type);
708 }
709 
712 {
713 public:
714  explicit c_enum_tag_typet(const irep_idt &identifier):
715  tag_typet(ID_c_enum_tag, identifier)
716  {
717  }
718 };
719 
723 template <>
724 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
725 {
726  return type.id() == ID_c_enum_tag;
727 }
728 
737 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
738 {
740  return static_cast<const c_enum_tag_typet &>(type);
741 }
742 
745 {
747  return static_cast<c_enum_tag_typet &>(type);
748 }
749 
751 class code_typet:public typet
752 {
753 public:
754  class parametert;
755  typedef std::vector<parametert> parameterst;
756 
760  code_typet(parameterst &&_parameters, typet &&_return_type) : typet(ID_code)
761  {
762  parameters().swap(_parameters);
763  return_type().swap(_return_type);
764  }
765 
769  code_typet(parameterst &&_parameters, const typet &_return_type)
770  : typet(ID_code)
771  {
772  parameters().swap(_parameters);
773  return_type() = _return_type;
774  }
775 
777  DEPRECATED("Use the two argument constructor instead")
778  code_typet():typet(ID_code)
779  {
780  // make sure these properties are always there to avoid problems
781  // with irept comparisons
782  add(ID_parameters);
783  add_type(ID_return_type);
784  }
785 
786  // used to be argumentt -- now uses standard terminology
787 
788  class parametert:public exprt
789  {
790  public:
791  DEPRECATED("use parametert(type) instead")
792  parametert():exprt(ID_parameter)
793  {
794  }
795 
796  explicit parametert(const typet &type):exprt(ID_parameter, type)
797  {
798  }
799 
800  const exprt &default_value() const
801  {
802  return find_expr(ID_C_default_value);
803  }
804 
805  bool has_default_value() const
806  {
807  return default_value().is_not_nil();
808  }
809 
811  {
812  return add_expr(ID_C_default_value);
813  }
814 
815  // The following for methods will go away;
816  // these should not be part of the signature of a function,
817  // but rather part of the body.
818  void set_identifier(const irep_idt &identifier)
819  {
820  set(ID_C_identifier, identifier);
821  }
822 
823  void set_base_name(const irep_idt &name)
824  {
825  set(ID_C_base_name, name);
826  }
827 
828  const irep_idt &get_identifier() const
829  {
830  return get(ID_C_identifier);
831  }
832 
833  const irep_idt &get_base_name() const
834  {
835  return get(ID_C_base_name);
836  }
837 
838  bool get_this() const
839  {
840  return get_bool(ID_C_this);
841  }
842 
843  void set_this()
844  {
845  set(ID_C_this, true);
846  }
847  };
848 
849  bool has_ellipsis() const
850  {
851  return find(ID_parameters).get_bool(ID_ellipsis);
852  }
853 
854  bool has_this() const
855  {
856  return get_this() != nullptr;
857  }
858 
859  const parametert *get_this() const
860  {
861  const parameterst &p=parameters();
862  if(!p.empty() && p.front().get_this())
863  return &p.front();
864  else
865  return nullptr;
866  }
867 
868  bool is_KnR() const
869  {
870  return get_bool(ID_C_KnR);
871  }
872 
874  {
875  add(ID_parameters).set(ID_ellipsis, true);
876  }
877 
879  {
880  add(ID_parameters).remove(ID_ellipsis);
881  }
882 
883  const typet &return_type() const
884  {
885  return find_type(ID_return_type);
886  }
887 
889  {
890  return add_type(ID_return_type);
891  }
892 
893  const parameterst &parameters() const
894  {
895  return (const parameterst &)find(ID_parameters).get_sub();
896  }
897 
899  {
900  return (parameterst &)add(ID_parameters).get_sub();
901  }
902 
903  bool get_inlined() const
904  {
905  return get_bool(ID_C_inlined);
906  }
907 
908  void set_inlined(bool value)
909  {
910  set(ID_C_inlined, value);
911  }
912 
913  const irep_idt &get_access() const
914  {
915  return get(ID_access);
916  }
917 
918  void set_access(const irep_idt &access)
919  {
920  return set(ID_access, access);
921  }
922 
923  bool get_is_constructor() const
924  {
925  return get_bool(ID_constructor);
926  }
927 
929  {
930  set(ID_constructor, true);
931  }
932 
934  std::vector<irep_idt> parameter_identifiers() const
935  {
936  std::vector<irep_idt> result;
937  const parameterst &p=parameters();
938  result.reserve(p.size());
939  for(parameterst::const_iterator it=p.begin();
940  it!=p.end(); it++)
941  result.push_back(it->get_identifier());
942  return result;
943  }
944 
945  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
946 
949  {
951  const parameterst &p = parameters();
952  parameter_indices.reserve(p.size());
953  std::size_t index = 0;
954  for(const auto &p : parameters())
955  {
956  const irep_idt &id = p.get_identifier();
957  if(!id.empty())
958  parameter_indices.insert({ id, index });
959  ++index;
960  }
961  return parameter_indices;
962  }
963 };
964 
968 template <>
969 inline bool can_cast_type<code_typet>(const typet &type)
970 {
971  return type.id() == ID_code;
972 }
973 
982 inline const code_typet &to_code_type(const typet &type)
983 {
985  validate_type(type);
986  return static_cast<const code_typet &>(type);
987 }
988 
991 {
993  validate_type(type);
994  return static_cast<code_typet &>(type);
995 }
996 
1001 {
1002 public:
1004  const typet &_subtype,
1005  const exprt &_size):type_with_subtypet(ID_array, _subtype)
1006  {
1007  size()=_size;
1008  }
1009 
1010  const exprt &size() const
1011  {
1012  return static_cast<const exprt &>(find(ID_size));
1013  }
1014 
1016  {
1017  return static_cast<exprt &>(add(ID_size));
1018  }
1019 
1020  bool is_complete() const
1021  {
1022  return size().is_not_nil();
1023  }
1024 
1025  bool is_incomplete() const
1026  {
1027  return size().is_nil();
1028  }
1029 };
1030 
1034 template <>
1035 inline bool can_cast_type<array_typet>(const typet &type)
1036 {
1037  return type.id() == ID_array;
1038 }
1039 
1048 inline const array_typet &to_array_type(const typet &type)
1049 {
1051  return static_cast<const array_typet &>(type);
1052 }
1053 
1056 {
1058  return static_cast<array_typet &>(type);
1059 }
1060 
1063 {
1064 public:
1066  {
1067  }
1068 };
1069 
1073 template <>
1075 {
1076  return type.id() == ID_incomplete_array;
1077 }
1078 
1088 {
1090  return static_cast<const incomplete_array_typet &>(type);
1091 }
1092 
1095 {
1097  return static_cast<incomplete_array_typet &>(type);
1098 }
1099 
1105 class bitvector_typet : public typet
1106 {
1107 public:
1108  explicit bitvector_typet(const irep_idt &_id) : typet(_id)
1109  {
1110  }
1111 
1112  bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
1113  {
1114  set_width(width);
1115  }
1116 
1117  std::size_t get_width() const
1118  {
1119  return get_size_t(ID_width);
1120  }
1121 
1122  void set_width(std::size_t width)
1123  {
1124  set(ID_width, width);
1125  }
1126 
1127  static void check(
1128  const typet &type,
1130  {
1131  DATA_CHECK(
1132  vm, !type.get(ID_width).empty(), "bitvector type must have width");
1133  }
1134 };
1135 
1139 template <>
1140 inline bool can_cast_type<bitvector_typet>(const typet &type)
1141 {
1142  return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
1143  type.id() == ID_fixedbv || type.id() == ID_floatbv ||
1144  type.id() == ID_verilog_signedbv ||
1145  type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
1146  type.id() == ID_pointer || type.id() == ID_c_bit_field ||
1147  type.id() == ID_c_bool;
1148 }
1149 
1158 inline const bitvector_typet &to_bitvector_type(const typet &type)
1159 {
1161 
1162  return static_cast<const bitvector_typet &>(type);
1163 }
1164 
1167 {
1169 
1170  return static_cast<bitvector_typet &>(type);
1171 }
1172 
1175 {
1176 public:
1177  explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
1178  {
1179  set_width(width);
1180  }
1181 };
1182 
1186 template <>
1187 inline bool can_cast_type<bv_typet>(const typet &type)
1188 {
1189  return type.id() == ID_bv;
1190 }
1191 
1192 inline void validate_type(const bv_typet &type)
1193 {
1194  DATA_INVARIANT(!type.get(ID_width).empty(), "bitvector type must have width");
1195 }
1196 
1205 inline const bv_typet &to_bv_type(const typet &type)
1206 {
1208  const bv_typet &ret = static_cast<const bv_typet &>(type);
1209  validate_type(ret);
1210  return ret;
1211 }
1212 
1214 inline bv_typet &to_bv_type(typet &type)
1215 {
1217  bv_typet &ret = static_cast<bv_typet &>(type);
1218  validate_type(ret);
1219  return ret;
1220 }
1221 
1224 {
1225 public:
1226  explicit unsignedbv_typet(std::size_t width):
1227  bitvector_typet(ID_unsignedbv, width)
1228  {
1229  }
1230 
1231  mp_integer smallest() const;
1232  mp_integer largest() const;
1233  constant_exprt smallest_expr() const;
1234  constant_exprt zero_expr() const;
1235  constant_exprt largest_expr() const;
1236 
1237  static void check(
1238  const typet &type,
1240  {
1241  bitvector_typet::check(type, vm);
1242  }
1243 };
1244 
1248 template <>
1249 inline bool can_cast_type<unsignedbv_typet>(const typet &type)
1250 {
1251  return type.id() == ID_unsignedbv;
1252 }
1253 
1262 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
1263 {
1266  return static_cast<const unsignedbv_typet &>(type);
1267 }
1268 
1271 {
1274  return static_cast<unsignedbv_typet &>(type);
1275 }
1276 
1279 {
1280 public:
1281  explicit signedbv_typet(std::size_t width):
1282  bitvector_typet(ID_signedbv, width)
1283  {
1284  }
1285 
1286  mp_integer smallest() const;
1287  mp_integer largest() const;
1288  constant_exprt smallest_expr() const;
1289  constant_exprt zero_expr() const;
1290  constant_exprt largest_expr() const;
1291 };
1292 
1296 template <>
1297 inline bool can_cast_type<signedbv_typet>(const typet &type)
1298 {
1299  return type.id() == ID_signedbv;
1300 }
1301 
1302 inline void validate_type(const signedbv_typet &type)
1303 {
1305  !type.get(ID_width).empty(), "signed bitvector type must have width");
1306 }
1307 
1316 inline const signedbv_typet &to_signedbv_type(const typet &type)
1317 {
1319  const signedbv_typet &ret = static_cast<const signedbv_typet &>(type);
1320  validate_type(ret);
1321  return ret;
1322 }
1323 
1326 {
1328  signedbv_typet &ret = static_cast<signedbv_typet &>(type);
1329  validate_type(ret);
1330  return ret;
1331 }
1332 
1338 {
1339 public:
1341  {
1342  }
1343 
1344  std::size_t get_fraction_bits() const
1345  {
1346  return get_width()-get_integer_bits();
1347  }
1348 
1349  std::size_t get_integer_bits() const;
1350 
1351  void set_integer_bits(std::size_t b)
1352  {
1353  set(ID_integer_bits, b);
1354  }
1355 };
1356 
1360 template <>
1361 inline bool can_cast_type<fixedbv_typet>(const typet &type)
1362 {
1363  return type.id() == ID_fixedbv;
1364 }
1365 
1366 inline void validate_type(const fixedbv_typet &type)
1367 {
1369  !type.get(ID_width).empty(), "fixed bitvector type must have width");
1370 }
1371 
1380 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
1381 {
1383  const fixedbv_typet &ret = static_cast<const fixedbv_typet &>(type);
1384  validate_type(ret);
1385  return ret;
1386 }
1387 
1390 {
1392  fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
1393  validate_type(ret);
1394  return ret;
1395 }
1396 
1399 {
1400 public:
1402  {
1403  }
1404 
1405  std::size_t get_e() const
1406  {
1407  // subtract one for sign bit
1408  return get_width()-get_f()-1;
1409  }
1410 
1411  std::size_t get_f() const;
1412 
1413  void set_f(std::size_t b)
1414  {
1415  set(ID_f, b);
1416  }
1417 };
1418 
1422 template <>
1423 inline bool can_cast_type<floatbv_typet>(const typet &type)
1424 {
1425  return type.id() == ID_floatbv;
1426 }
1427 
1428 inline void validate_type(const floatbv_typet &type)
1429 {
1431  !type.get(ID_width).empty(), "float bitvector type must have width");
1432 }
1433 
1442 inline const floatbv_typet &to_floatbv_type(const typet &type)
1443 {
1445  const floatbv_typet &ret = static_cast<const floatbv_typet &>(type);
1446  validate_type(ret);
1447  return ret;
1448 }
1449 
1452 {
1454  floatbv_typet &ret = static_cast<floatbv_typet &>(type);
1455  validate_type(ret);
1456  return ret;
1457 }
1458 
1463 {
1464 public:
1465  explicit c_bit_field_typet(const typet &_subtype, std::size_t width)
1466  : bitvector_typet(ID_c_bit_field, width)
1467  {
1468  subtype() = _subtype;
1469  }
1470 
1471  // These have a sub-type
1472 };
1473 
1477 template <>
1478 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
1479 {
1480  return type.id() == ID_c_bit_field;
1481 }
1482 
1491 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
1492 {
1494  return static_cast<const c_bit_field_typet &>(type);
1495 }
1496 
1499 {
1501  return static_cast<c_bit_field_typet &>(type);
1502 }
1503 
1508 {
1509 public:
1510  pointer_typet(const typet &_subtype, std::size_t width)
1511  : bitvector_typet(ID_pointer, width)
1512  {
1513  subtype() = _subtype;
1514  }
1515 
1517  {
1518  return signedbv_typet(get_width());
1519  }
1520 };
1521 
1525 template <>
1526 inline bool can_cast_type<pointer_typet>(const typet &type)
1527 {
1528  return type.id() == ID_pointer;
1529 }
1530 
1531 inline void validate_type(const pointer_typet &type)
1532 {
1533  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
1534 }
1535 
1544 inline const pointer_typet &to_pointer_type(const typet &type)
1545 {
1547  const pointer_typet &ret = static_cast<const pointer_typet &>(type);
1548  validate_type(ret);
1549  return ret;
1550 }
1551 
1554 {
1556  pointer_typet &ret = static_cast<pointer_typet &>(type);
1557  validate_type(ret);
1558  return ret;
1559 }
1560 
1566 {
1567 public:
1568  reference_typet(const typet &_subtype, std::size_t _width):
1569  pointer_typet(_subtype, _width)
1570  {
1571  set(ID_C_reference, true);
1572  }
1573 };
1574 
1578 template <>
1579 inline bool can_cast_type<reference_typet>(const typet &type)
1580 {
1581  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference) &&
1582  !type.get(ID_width).empty();
1583 }
1584 
1593 inline const reference_typet &to_reference_type(const typet &type)
1594 {
1596  return static_cast<const reference_typet &>(type);
1597 }
1598 
1601 {
1603  return static_cast<reference_typet &>(type);
1604 }
1605 
1606 bool is_reference(const typet &type);
1607 
1608 bool is_rvalue_reference(const typet &type);
1609 
1612 {
1613 public:
1614  explicit c_bool_typet(std::size_t width):
1615  bitvector_typet(ID_c_bool, width)
1616  {
1617  }
1618 };
1619 
1623 template <>
1624 inline bool can_cast_type<c_bool_typet>(const typet &type)
1625 {
1626  return type.id() == ID_c_bool;
1627 }
1628 
1629 inline void validate_type(const c_bool_typet &type)
1630 {
1631  DATA_INVARIANT(!type.get(ID_width).empty(), "C bool type must have width");
1632 }
1633 
1642 inline const c_bool_typet &to_c_bool_type(const typet &type)
1643 {
1645  const c_bool_typet &ret = static_cast<const c_bool_typet &>(type);
1646  validate_type(ret);
1647  return ret;
1648 }
1649 
1652 {
1654  c_bool_typet &ret = static_cast<c_bool_typet &>(type);
1655  validate_type(ret);
1656  return ret;
1657 }
1658 
1662 class string_typet:public typet
1663 {
1664 public:
1665  string_typet():typet(ID_string)
1666  {
1667  }
1668 };
1669 
1673 template <>
1674 inline bool can_cast_type<string_typet>(const typet &type)
1675 {
1676  return type.id() == ID_string;
1677 }
1678 
1687 inline const string_typet &to_string_type(const typet &type)
1688 {
1690  return static_cast<const string_typet &>(type);
1691 }
1692 
1695 {
1697  return static_cast<string_typet &>(type);
1698 }
1699 
1701 class range_typet:public typet
1702 {
1703 public:
1704  range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
1705  {
1706  set_from(_from);
1707  set_to(_to);
1708  }
1709 
1710  mp_integer get_from() const;
1711  mp_integer get_to() const;
1712 
1713  void set_from(const mp_integer &_from);
1714  void set_to(const mp_integer &to);
1715 };
1716 
1720 template <>
1721 inline bool can_cast_type<range_typet>(const typet &type)
1722 {
1723  return type.id() == ID_range;
1724 }
1725 
1734 inline const range_typet &to_range_type(const typet &type)
1735 {
1737  return static_cast<const range_typet &>(type);
1738 }
1739 
1742 {
1744  return static_cast<range_typet &>(type);
1745 }
1746 
1756 {
1757 public:
1759  const typet &_subtype,
1760  const exprt &_size):type_with_subtypet(ID_vector, _subtype)
1761  {
1762  size()=_size;
1763  }
1764 
1765  const exprt &size() const
1766  {
1767  return static_cast<const exprt &>(find(ID_size));
1768  }
1769 
1771  {
1772  return static_cast<exprt &>(add(ID_size));
1773  }
1774 };
1775 
1779 template <>
1780 inline bool can_cast_type<vector_typet>(const typet &type)
1781 {
1782  return type.id() == ID_vector;
1783 }
1784 
1793 inline const vector_typet &to_vector_type(const typet &type)
1794 {
1796  return static_cast<const vector_typet &>(type);
1797 }
1798 
1801 {
1803  return static_cast<vector_typet &>(type);
1804 }
1805 
1808 {
1809 public:
1810  DEPRECATED("use complex_typet(type) instead")
1812  {
1813  }
1814 
1815  explicit complex_typet(const typet &_subtype):
1816  type_with_subtypet(ID_complex, _subtype)
1817  {
1818  }
1819 };
1820 
1824 template <>
1825 inline bool can_cast_type<complex_typet>(const typet &type)
1826 {
1827  return type.id() == ID_complex;
1828 }
1829 
1838 inline const complex_typet &to_complex_type(const typet &type)
1839 {
1841  return static_cast<const complex_typet &>(type);
1842 }
1843 
1846 {
1848  return static_cast<complex_typet &>(type);
1849 }
1850 
1852  const typet &type,
1853  const namespacet &ns);
1854 
1855 #endif // CPROVER_UTIL_STD_TYPES_H
The void type, the same as empty_typet.
Definition: std_types.h:57
const irept & get_nil_irep()
Definition: irep.cpp:55
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1127
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:969
const irep_idt & get_name() const
Definition: std_types.h:132
The type of an expression, extends irept.
Definition: type.h:27
std::size_t get_e() const
Definition: std_types.h:1405
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:464
c_enum_typet(const typet &_subtype)
Definition: std_types.h:650
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
Definition: std_types.h:1674
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
c_bit_field_typet(const typet &_subtype, std::size_t width)
Definition: std_types.h:1465
constant_exprt zero_expr() const
Definition: std_types.cpp:200
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:570
void set_access(const irep_idt &access)
Definition: std_types.h:918
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
code_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e., function type.
Definition: std_types.h:769
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1140
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:751
const irep_idt & get_identifier() const
Definition: std_types.h:479
array_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1003
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:139
constant_exprt largest_expr() const
Definition: std_types.cpp:210
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
tag_typet(const irep_idt &_id, const irep_idt &identifier)
Definition: std_types.h:467
c_bool_typet(std::size_t width)
Definition: std_types.h:1614
signedbv_typet(std::size_t width)
Definition: std_types.h:1281
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: std_types.h:1593
void validate_type(const bv_typet &type)
Definition: std_types.h:1192
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition: std_types.h:1035
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
std::vector< irept > subt
Definition: irep.h:160
An enumeration type, i.e., a type with elements (not to be confused with C enums) ...
Definition: std_types.h:598
bool can_cast_type< incomplete_array_typet >(const typet &type)
Check whether a reference to a typet is a incomplete_array_typet.
Definition: std_types.h:1074
reference_typet(const typet &_subtype, std::size_t _width)
Definition: std_types.h:1568
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_typet.
Definition: std_types.h:489
exprt & size()
Definition: std_types.h:1770
bool has_ellipsis() const
Definition: std_types.h:849
Arrays without size.
Definition: std_types.h:1062
bool_typet()
Definition: std_types.h:31
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:147
void set_name(const irep_idt &name)
Definition: std_types.h:137
std::size_t get_integer_bits() const
Definition: std_types.cpp:20
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition: std_types.h:1721
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:503
std::vector< componentt > componentst
Definition: std_types.h:203
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:1112
std::vector< parametert > parameterst
Definition: std_types.h:754
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition: std_types.h:237
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:557
const componentst & components() const
Definition: std_types.h:205
bool is_incomplete() const
Definition: std_types.h:1025
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:299
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:70
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
const memberst & members() const
Definition: std_types.h:674
typet & type()
Return the type of the expression.
Definition: expr.h:68
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:661
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:409
The Boolean type.
Definition: std_types.h:28
A constant literal expression.
Definition: std_expr.h:4384
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool get_is_constructor() const
Definition: std_types.h:923
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
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:724
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:474
unsignedbv_typet(std::size_t width)
Definition: std_types.h:1226
Type for C bit fields These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (...
Definition: std_types.h:1462
bool has_default_value() const
Definition: std_types.h:805
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:1108
subt & get_sub()
Definition: irep.h:317
componentst & methods()
Definition: std_types.h:381
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1642
void set_base_name(const irep_idt &name)
Definition: std_types.h:823
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1526
String type.
Definition: std_types.h:1662
Templated functions to cast to specific exprt-derived classes.
const irep_idt & get_base_name() const
Definition: std_types.h:142
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:117
void set_is_constructor()
Definition: std_types.h:928
bool can_cast_type< struct_typet >(const typet &type)
Check whether a reference to a typet is a struct_typet.
Definition: std_types.h:336
mp_integer get_to() const
Definition: std_types.cpp:160
const irep_idt & id() const
Definition: irep.h:259
void set_is_padding(bool is_padding)
Definition: std_types.h:187
exprt & size()
Definition: std_types.h:1015
const irep_idt & get_base_name() const
Definition: std_types.h:833
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition: std_types.h:934
void set_inlined(bool value)
Definition: std_types.h:908
const methodst & methods() const
Definition: std_types.h:376
bool can_cast_type< bv_typet >(const typet &type)
Check whether a reference to a typet is a bv_typet.
Definition: std_types.h:1187
void set_value(const irep_idt &value)
Definition: std_types.h:659
nil_typet()
Definition: std_types.h:42
void remove_ellipsis()
Definition: std_types.h:878
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
constant_exprt smallest_expr() const
Definition: std_types.cpp:180
A reference into the symbol table.
Definition: std_types.h:62
irep_idt get_identifier() const
Definition: std_types.h:660
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: std_types.h:1579
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:633
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition: std_types.h:945
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
symbol_typet(const irep_idt &identifier)
Definition: std_types.h:65
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
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:247
The empty type.
Definition: std_types.h:48
std::size_t get_fraction_bits() const
Definition: std_types.h:1344
void set_access(const irep_idt &access)
Definition: std_types.h:157
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1278
const parametert * get_this() const
Definition: std_types.h:859
The vector type.
Definition: std_types.h:1755
nonstd::optional< T > optionalt
Definition: optional.h:35
void set_integer_bits(std::size_t b)
Definition: std_types.h:1351
bool can_cast_type< fixedbv_typet >(const typet &type)
Check whether a reference to a typet is a fixedbv_typet.
Definition: std_types.h:1361
componentst & components()
Definition: std_types.h:210
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
Definition: std_types.h:1423
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:1704
void set_is_final(const bool is_final)
Definition: std_types.h:197
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const exprt & size() const
Definition: std_types.h:1765
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
Definition: std_types.h:326
vector_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1758
void set_tag(const irep_idt &tag)
Definition: std_types.h:227
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
mp_integer smallest() const
Definition: std_types.cpp:190
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:87
const exprt & size() const
Definition: std_types.h:1010
Base class for tree-like data structures with sharing.
Definition: irep.h:156
void set_from(const mp_integer &_from)
Definition: std_types.cpp:145
signedbv_typet difference_type() const
Definition: std_types.h:1516
bv_typet(std::size_t width)
Definition: std_types.h:1177
Type with a single subtype.
Definition: type.h:135
mp_integer largest() const
Definition: std_types.cpp:195
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
mp_integer smallest() const
Definition: std_types.cpp:165
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
Definition: std_types.h:1825
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const irep_idt & get_access() const
Definition: std_types.h:913
pointer_typet(const typet &_subtype, std::size_t width)
Definition: std_types.h:1510
bool get_this() const
Definition: std_types.h:838
complex_typet(const typet &_subtype)
Definition: std_types.h:1815
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1337
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1205
Base class of fixed-width bit-vector types.
Definition: std_types.h:1105
const irept::subt & elements() const
Definition: std_types.h:605
std::size_t get_width() const
Definition: std_types.h:1117
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:737
const irep_idt & get_pretty_name() const
Definition: std_types.h:162
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:1237
void make_ellipsis()
Definition: std_types.h:873
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a typet to an incomplete_array_typet.
Definition: std_types.h:1087
The reference type.
Definition: std_types.h:1565
componentt methodt
Definition: std_types.h:373
std::size_t get_f() const
Definition: std_types.cpp:27
#define DEPRECATED(msg)
Definition: deprecate.h:23
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
Complex numbers made of pair of given subtype.
Definition: std_types.h:1807
typet & return_type()
Definition: std_types.h:888
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:818
mp_integer largest() const
Definition: std_types.cpp:170
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:106
bool is_KnR() const
Definition: std_types.h:868
constant_exprt largest_expr() const
Definition: std_types.cpp:185
const irep_idt & get_access() const
Definition: std_types.h:152
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:92
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Definition: std_types.h:1249
Base type for structs and unions.
Definition: std_types.h:114
Base class or struct that a class or struct inherits from.
Definition: std_types.h:292
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
Definition: std_types.h:437
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition: std_types.h:948
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition: std_types.h:1780
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const typet & find_type(const irep_namet &name) const
Definition: type.h:77
The union type.
Definition: std_types.h:425
const parameterst & parameters() const
Definition: std_types.h:893
exprt & default_value()
Definition: std_types.h:810
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:35
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
bool has_this() const
Definition: std_types.h:854
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:167
A type for subranges of integers.
Definition: std_types.h:1701
bool is_abstract() const
Definition: std_types.h:386
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
constant_exprt smallest_expr() const
Definition: std_types.cpp:205
irept & add(const irep_namet &name)
Definition: irep.cpp:305
typet & add_type(const irep_namet &name)
Definition: type.h:72
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:224
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
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:530
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
void swap(irept &irep)
Definition: irep.h:303
bool is_complete() const
Definition: std_types.h:1020
baset(const struct_tag_typet &base)
Definition: std_types.cpp:83
void set_f(std::size_t b)
Definition: std_types.h:1413
Arrays with given size.
Definition: std_types.h:1000
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:1491
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition: std_types.h:1687
validation_modet
void set_anonymous(bool anonymous)
Definition: std_types.h:177
irept::subt & elements()
Definition: std_types.h:610
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:286
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
Definition: std_types.h:1297
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1734
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:520
exprt & add_expr(const irep_idt &name)
Definition: expr.h:294
void remove(const irep_namet &name)
Definition: irep.cpp:269
The C/C++ Booleans.
Definition: std_types.h:1611
basest & bases()
Get the collection of base classes/structs.
Definition: std_types.h:309
const typet & subtype() const
Definition: type.h:38
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:684
irep_idt get_tag() const
Definition: std_types.h:226
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
Class type.
Definition: std_types.h:365
parametert(const typet &type)
Definition: std_types.h:796
bool get_inlined() const
Definition: std_types.h:903
parameterst & parameters()
Definition: std_types.h:898
void set_to(const mp_integer &to)
Definition: std_types.cpp:150
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1174
std::vector< baset > basest
Definition: std_types.h:300
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
irep_idt get_base_name() const
Definition: std_types.h:665
c_enum_tag_typet(const irep_idt &identifier)
Definition: std_types.h:714
code_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e., function type.
Definition: std_types.h:760
const irep_idt & get_identifier() const
Definition: std_types.h:828
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:1624
std::vector< c_enum_membert > memberst
Definition: std_types.h:672
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
The type of C enums.
Definition: std_types.h:647
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:230
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
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:1478
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition: std_types.h:396
const typet & return_type() const
Definition: std_types.h:883
bool can_cast_type< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
Definition: std_types.h:620
bool can_cast_type< symbol_typet >(const typet &type)
Check whether a reference to a typet is a symbol_typet.
Definition: std_types.h:85
const irep_idt & get_identifier() const
Definition: std_types.h:75
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:666
const exprt & default_value() const
Definition: std_types.h:800
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
componentt(const irep_idt &_name, const typet &_type)
Definition: std_types.h:126
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
union_tag_typet(const irep_idt &identifier)
Definition: std_types.h:560
componentst methodst
Definition: std_types.h:374
struct_tag_typet & type()
Definition: std_types.cpp:73
void set_width(std::size_t width)
Definition: std_types.h:1122
irep_idt get_value() const
Definition: std_types.h:658
constant_exprt zero_expr() const
Definition: std_types.cpp:175
mp_integer get_from() const
Definition: std_types.cpp:155