cprover
std_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_TYPES_H
11 #define CPROVER_UTIL_STD_TYPES_H
12 
20 #include <cassert>
21 
22 #include "expr.h"
23 #include "mp_arith.h"
24 
25 class constant_exprt;
26 
33 class bool_typet:public typet
34 {
35 public:
36  bool_typet():typet(ID_bool)
37  {
38  }
39 };
40 
43 class nil_typet:public typet
44 {
45 public:
46  nil_typet():typet(static_cast<const typet &>(get_nil_irep()))
47  {
48  }
49 };
50 
53 class empty_typet:public typet
54 {
55 public:
56  empty_typet():typet(ID_empty)
57  {
58  }
59 };
60 
63 class void_typet:public empty_typet
64 {
65 };
66 
69 class integer_typet:public typet
70 {
71 public:
72  integer_typet():typet(ID_integer)
73  {
74  }
75 };
76 
79 class natural_typet:public typet
80 {
81 public:
82  natural_typet():typet(ID_natural)
83  {
84  }
85 };
86 
89 class rational_typet:public typet
90 {
91 public:
92  rational_typet():typet(ID_rational)
93  {
94  }
95 };
96 
99 class real_typet:public typet
100 {
101 public:
102  real_typet():typet(ID_real)
103  {
104  }
105 };
106 
109 class symbol_typet:public typet
110 {
111 public:
112  symbol_typet():typet(ID_symbol)
113  {
114  }
115 
116  explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
117  {
118  set_identifier(identifier);
119  }
120 
121  void set_identifier(const irep_idt &identifier)
122  {
123  set(ID_identifier, identifier);
124  }
125 
126  const irep_idt &get_identifier() const
127  {
128  return get(ID_identifier);
129  }
130 };
131 
142 inline const symbol_typet &to_symbol_type(const typet &type)
143 {
144  assert(type.id()==ID_symbol);
145  return static_cast<const symbol_typet &>(type);
146 }
147 
152 {
153  assert(type.id()==ID_symbol);
154  return static_cast<symbol_typet &>(type);
155 }
156 
160 {
161 public:
162  explicit struct_union_typet(const irep_idt &_id):typet(_id)
163  {
164  }
165 
166  class componentt:public exprt
167  {
168  public:
170  {
171  }
172 
173  componentt(const irep_idt &_name, const typet &_type)
174  {
175  set_name(_name);
176  type()=_type;
177  }
178 
179  const irep_idt &get_name() const
180  {
181  return get(ID_name);
182  }
183 
184  void set_name(const irep_idt &name)
185  {
186  return set(ID_name, name);
187  }
188 
189  const irep_idt &get_base_name() const
190  {
191  return get(ID_base_name);
192  }
193 
194  void set_base_name(const irep_idt &base_name)
195  {
196  return set(ID_base_name, base_name);
197  }
198 
199  const irep_idt &get_access() const
200  {
201  return get(ID_access);
202  }
203 
204  void set_access(const irep_idt &access)
205  {
206  return set(ID_access, access);
207  }
208 
209  const irep_idt &get_pretty_name() const
210  {
211  return get(ID_pretty_name);
212  }
213 
214  void set_pretty_name(const irep_idt &name)
215  {
216  return set(ID_pretty_name, name);
217  }
218 
219  bool get_anonymous() const
220  {
221  return get_bool(ID_anonymous);
222  }
223 
224  void set_anonymous(bool anonymous)
225  {
226  return set(ID_anonymous, anonymous);
227  }
228 
229  bool get_is_padding() const
230  {
231  return get_bool(ID_C_is_padding);
232  }
233 
234  void set_is_padding(bool is_padding)
235  {
236  return set(ID_C_is_padding, is_padding);
237  }
238  };
239 
240  typedef std::vector<componentt> componentst;
241 
242  const componentst &components() const
243  {
244  return (const componentst &)(find(ID_components).get_sub());
245  }
246 
248  {
249  return (componentst &)(add(ID_components).get_sub());
250  }
251 
252  bool has_component(const irep_idt &component_name) const
253  {
254  return get_component(component_name).is_not_nil();
255  }
256 
257  const componentt &get_component(
258  const irep_idt &component_name) const;
259 
260  std::size_t component_number(const irep_idt &component_name) const;
261  typet component_type(const irep_idt &component_name) const;
262 
263  irep_idt get_tag() const { return get(ID_tag); }
264  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
265 };
266 
278 {
279  assert(type.id()==ID_struct ||
280  type.id()==ID_union);
281  return static_cast<const struct_union_typet &>(type);
282 }
283 
288 {
289  assert(type.id()==ID_struct ||
290  type.id()==ID_union);
291  return static_cast<struct_union_typet &>(type);
292 }
293 
297 {
298 public:
300  {
301  }
302 
303  // returns true if the object is a prefix of \a other
304  bool is_prefix_of(const struct_typet &other) const;
305 };
306 
317 inline const struct_typet &to_struct_type(const typet &type)
318 {
319  assert(type.id()==ID_struct);
320  return static_cast<const struct_typet &>(type);
321 }
322 
327 {
328  assert(type.id()==ID_struct);
329  return static_cast<struct_typet &>(type);
330 }
331 
335 {
336 public:
338  {
339  set(ID_C_class, true);
340  }
341 
344 
345  const methodst &methods() const
346  {
347  return (const methodst &)(find(ID_methods).get_sub());
348  }
349 
351  {
352  return (methodst &)(add(ID_methods).get_sub());
353  }
354 
355  bool is_class() const
356  {
357  return get_bool(ID_C_class);
358  }
359 
361  {
362  return is_class()?ID_private:ID_public;
363  }
364 
365  const irept::subt &bases() const
366  {
367  return find(ID_bases).get_sub();
368  }
369 
371  {
372  return add(ID_bases).get_sub();
373  }
374 
375  void add_base(const typet &base)
376  {
377  bases().push_back(exprt(ID_base, base));
378  }
379 
380  bool has_base(const irep_idt &id) const
381  {
382  const irept::subt &b=bases();
383 
384  forall_irep(it, b)
385  {
386  assert(it->id()==ID_base);
387  const irept &type=it->find(ID_type);
388  assert(type.id()==ID_symbol);
389  if(type.get(ID_identifier)==id)
390  return true;
391  }
392 
393  return false;
394  }
395 };
396 
407 inline const class_typet &to_class_type(const typet &type)
408 {
409  assert(type.id()==ID_struct);
410  return static_cast<const class_typet &>(type);
411 }
412 
417 {
418  assert(type.id()==ID_struct);
419  return static_cast<class_typet &>(type);
420 }
421 
425 {
426 public:
428  {
429  }
430 };
431 
442 inline const union_typet &to_union_type(const typet &type)
443 {
444  assert(type.id()==ID_union);
445  return static_cast<const union_typet &>(type);
446 }
447 
452 {
453  assert(type.id()==ID_union);
454  return static_cast<union_typet &>(type);
455 }
456 
460 class tag_typet:public typet
461 {
462 public:
463  explicit tag_typet(const irep_idt &_id):typet(_id)
464  {
465  }
466 
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 
495 inline const tag_typet &to_tag_type(const typet &type)
496 {
497  assert(type.id()==ID_c_enum_tag ||
498  type.id()==ID_struct_tag ||
499  type.id()==ID_union_tag);
500  return static_cast<const tag_typet &>(type);
501 }
502 
507 {
508  assert(type.id()==ID_c_enum_tag ||
509  type.id()==ID_struct_tag ||
510  type.id()==ID_union_tag);
511  return static_cast<tag_typet &>(type);
512 }
513 
518 {
519 public:
520  explicit struct_tag_typet(const irep_idt &identifier):
521  tag_typet(ID_struct_tag, identifier)
522  {
523  }
524 };
525 
536 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
537 {
538  assert(type.id()==ID_struct_tag);
539  return static_cast<const struct_tag_typet &>(type);
540 }
541 
546 {
547  assert(type.id()==ID_struct_tag);
548  return static_cast<struct_tag_typet &>(type);
549 }
550 
555 {
556 public:
557  explicit union_tag_typet(const irep_idt &identifier):
558  tag_typet(ID_union_tag, identifier)
559  {
560  }
561 };
562 
573 inline const union_tag_typet &to_union_tag_type(const typet &type)
574 {
575  assert(type.id()==ID_union_tag);
576  return static_cast<const union_tag_typet &>(type);
577 }
578 
583 {
584  assert(type.id()==ID_union_tag);
585  return static_cast<union_tag_typet &>(type);
586 }
587 
592 {
593 public:
594  enumeration_typet():typet(ID_enumeration)
595  {
596  }
597 
598  const irept::subt &elements() const
599  {
600  return find(ID_elements).get_sub();
601  }
602 
604  {
605  return add(ID_elements).get_sub();
606  }
607 };
608 
619 inline const enumeration_typet &to_enumeration_type(const typet &type)
620 {
621  assert(type.id()==ID_enumeration);
622  return static_cast<const enumeration_typet &>(type);
623 }
624 
629 {
630  assert(type.id()==ID_enumeration);
631  return static_cast<enumeration_typet &>(type);
632 }
633 
638 {
639 public:
640  explicit c_enum_typet(const typet &_subtype):
641  type_with_subtypet(ID_c_enum, _subtype)
642  {
643  }
644 
645  class c_enum_membert:public irept
646  {
647  public:
648  irep_idt get_value() const { return get(ID_value); }
649  void set_value(const irep_idt &value) { set(ID_value, value); }
650  irep_idt get_identifier() const { return get(ID_identifier); }
651  void set_identifier(const irep_idt &identifier)
652  {
653  set(ID_identifier, identifier);
654  }
655  irep_idt get_base_name() const { return get(ID_base_name); }
656  void set_base_name(const irep_idt &base_name)
657  {
658  set(ID_base_name, base_name);
659  }
660  };
661 
662  typedef std::vector<c_enum_membert> memberst;
663 
664  const memberst &members() const
665  {
666  return (const memberst &)(find(ID_body).get_sub());
667  }
668 };
669 
680 inline const c_enum_typet &to_c_enum_type(const typet &type)
681 {
682  assert(type.id()==ID_c_enum);
683  return static_cast<const c_enum_typet &>(type);
684 }
685 
690 {
691  assert(type.id()==ID_c_enum);
692  return static_cast<c_enum_typet &>(type);
693 }
694 
699 {
700 public:
701  explicit c_enum_tag_typet(const irep_idt &identifier):
702  tag_typet(ID_c_enum_tag, identifier)
703  {
704  }
705 };
706 
717 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
718 {
719  assert(type.id()==ID_c_enum_tag);
720  return static_cast<const c_enum_tag_typet &>(type);
721 }
722 
727 {
728  assert(type.id()==ID_c_enum_tag);
729  return static_cast<c_enum_tag_typet &>(type);
730 }
731 
734 class code_typet:public typet
735 {
736 public:
737  code_typet():typet(ID_code)
738  {
739  }
740 
741  // used to be argumentt -- now uses standard terminology
742 
743  class parametert:public exprt
744  {
745  public:
746  parametert():exprt(ID_parameter)
747  {
748  }
749 
750  explicit parametert(const typet &type):exprt(ID_parameter, type)
751  {
752  }
753 
754  const exprt &default_value() const
755  {
756  return find_expr(ID_C_default_value);
757  }
758 
759  bool has_default_value() const
760  {
761  return default_value().is_not_nil();
762  }
763 
765  {
766  return add_expr(ID_C_default_value);
767  }
768 
769  // The following for methods will go away;
770  // these should not be part of the signature of a function,
771  // but rather part of the body.
772  void set_identifier(const irep_idt &identifier)
773  {
774  set(ID_C_identifier, identifier);
775  }
776 
777  void set_base_name(const irep_idt &name)
778  {
779  set(ID_C_base_name, name);
780  }
781 
782  const irep_idt &get_identifier() const
783  {
784  return get(ID_C_identifier);
785  }
786 
787  const irep_idt &get_base_name() const
788  {
789  return get(ID_C_base_name);
790  }
791 
792  bool get_this() const
793  {
794  return get_bool(ID_C_this);
795  }
796 
797  void set_this()
798  {
799  set(ID_C_this, true);
800  }
801  };
802 
803  bool has_ellipsis() const
804  {
805  return find(ID_parameters).get_bool(ID_ellipsis);
806  }
807 
808  bool has_this() const
809  {
810  const parameterst &p=parameters();
811  return !p.empty() && p.front().get_this();
812  }
813 
814  bool is_KnR() const
815  {
816  return get_bool(ID_C_KnR);
817  }
818 
820  {
821  add(ID_parameters).set(ID_ellipsis, true);
822  }
823 
825  {
826  add(ID_parameters).remove(ID_ellipsis);
827  }
828 
829  typedef std::vector<parametert> parameterst;
830 
831  const typet &return_type() const
832  {
833  return find_type(ID_return_type);
834  }
835 
837  {
838  return add_type(ID_return_type);
839  }
840 
841  const parameterst &parameters() const
842  {
843  return (const parameterst &)find(ID_parameters).get_sub();
844  }
845 
847  {
848  return (parameterst &)add(ID_parameters).get_sub();
849  }
850 
851  bool get_inlined() const
852  {
853  return get_bool(ID_C_inlined);
854  }
855 
856  void set_inlined(bool value)
857  {
858  set(ID_C_inlined, value);
859  }
860 
861  // this produces the list of parameter identifiers
862  std::vector<irep_idt> parameter_identifiers() const
863  {
864  std::vector<irep_idt> result;
865  const parameterst &p=parameters();
866  result.reserve(p.size());
867  for(parameterst::const_iterator it=p.begin();
868  it!=p.end(); it++)
869  result.push_back(it->get_identifier());
870  return result;
871  }
872 };
873 
884 inline const code_typet &to_code_type(const typet &type)
885 {
886  assert(type.id()==ID_code);
887  return static_cast<const code_typet &>(type);
888 }
889 
894 {
895  assert(type.id()==ID_code);
896  return static_cast<code_typet &>(type);
897 }
898 
902 {
903 public:
905  {
906  }
907 
909  const typet &_subtype,
910  const exprt &_size):type_with_subtypet(ID_array, _subtype)
911  {
912  size()=_size;
913  }
914 
915  const exprt &size() const
916  {
917  return static_cast<const exprt &>(find(ID_size));
918  }
919 
921  {
922  return static_cast<exprt &>(add(ID_size));
923  }
924 
925  bool is_complete() const
926  {
927  return size().is_not_nil();
928  }
929 
930  bool is_incomplete() const
931  {
932  return size().is_nil();
933  }
934 };
935 
946 inline const array_typet &to_array_type(const typet &type)
947 {
948  assert(type.id()==ID_array);
949  return static_cast<const array_typet &>(type);
950 }
951 
956 {
957  assert(type.id()==ID_array);
958  return static_cast<array_typet &>(type);
959 }
960 
964 {
965 public:
967  {
968  }
969 
970  explicit incomplete_array_typet(const typet &_subtype):
971  type_with_subtypet(ID_array, _subtype)
972  {
973  }
974 };
975 
987 {
988  assert(type.id()==ID_array);
989  return static_cast<const incomplete_array_typet &>(type);
990 }
991 
996 {
997  assert(type.id()==ID_array);
998  return static_cast<incomplete_array_typet &>(type);
999 }
1000 
1004 {
1005 public:
1006  explicit bitvector_typet(const irep_idt &_id):type_with_subtypet(_id)
1007  {
1008  }
1009 
1010  bitvector_typet(const irep_idt &_id, const typet &_subtype):
1011  type_with_subtypet(_id, _subtype)
1012  {
1013  }
1014 
1016  const irep_idt &_id,
1017  const typet &_subtype,
1018  std::size_t width):
1019  type_with_subtypet(_id, _subtype)
1020  {
1021  set_width(width);
1022  }
1023 
1024  bitvector_typet(const irep_idt &_id, std::size_t width):
1025  type_with_subtypet(_id)
1026  {
1027  set_width(width);
1028  }
1029 
1030  std::size_t get_width() const
1031  {
1032  return get_size_t(ID_width);
1033  }
1034 
1035  void set_width(std::size_t width)
1036  {
1037  set(ID_width, width);
1038  }
1039 };
1040 
1051 inline const bitvector_typet &to_bitvector_type(const typet &type)
1052 {
1053  assert(type.id()==ID_signedbv ||
1054  type.id()==ID_unsignedbv ||
1055  type.id()==ID_fixedbv ||
1056  type.id()==ID_floatbv ||
1057  type.id()==ID_verilog_signedbv ||
1058  type.id()==ID_verilog_unsignedbv ||
1059  type.id()==ID_bv ||
1060  type.id()==ID_pointer ||
1061  type.id()==ID_c_bit_field ||
1062  type.id()==ID_c_bool);
1063 
1064  return static_cast<const bitvector_typet &>(type);
1065 }
1066 
1068 {
1069  assert(type.id()==ID_signedbv ||
1070  type.id()==ID_unsignedbv ||
1071  type.id()==ID_fixedbv ||
1072  type.id()==ID_floatbv ||
1073  type.id()==ID_verilog_signedbv ||
1074  type.id()==ID_verilog_unsignedbv ||
1075  type.id()==ID_bv ||
1076  type.id()==ID_pointer ||
1077  type.id()==ID_c_bit_field ||
1078  type.id()==ID_c_bool);
1079 
1080  return static_cast<bitvector_typet &>(type);
1081 }
1082 
1086 {
1087 public:
1089  {
1090  }
1091 
1092  explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
1093  {
1094  set_width(width);
1095  }
1096 };
1097 
1108 inline const bv_typet &to_bv_type(const typet &type)
1109 {
1110  assert(type.id()==ID_bv);
1111  return static_cast<const bv_typet &>(type);
1112 }
1113 
1117 inline bv_typet &to_bv_type(typet &type)
1118 {
1119  assert(type.id()==ID_bv);
1120  return static_cast<bv_typet &>(type);
1121 }
1122 
1126 {
1127 public:
1129  {
1130  }
1131 
1132  explicit unsignedbv_typet(std::size_t width):
1133  bitvector_typet(ID_unsignedbv, width)
1134  {
1135  }
1136 
1137  mp_integer smallest() const;
1138  mp_integer largest() const;
1139  constant_exprt smallest_expr() const;
1140  constant_exprt zero_expr() const;
1141  constant_exprt largest_expr() const;
1142 };
1143 
1154 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
1155 {
1156  assert(type.id()==ID_unsignedbv);
1157  return static_cast<const unsignedbv_typet &>(type);
1158 }
1159 
1164 {
1165  assert(type.id()==ID_unsignedbv);
1166  return static_cast<unsignedbv_typet &>(type);
1167 }
1168 
1172 {
1173 public:
1175  {
1176  }
1177 
1178  explicit signedbv_typet(std::size_t width):
1179  bitvector_typet(ID_signedbv, width)
1180  {
1181  }
1182 
1183  mp_integer smallest() const;
1184  mp_integer largest() const;
1185  constant_exprt smallest_expr() const;
1186  constant_exprt zero_expr() const;
1187  constant_exprt largest_expr() const;
1188 };
1189 
1200 inline const signedbv_typet &to_signedbv_type(const typet &type)
1201 {
1202  assert(type.id()==ID_signedbv);
1203  return static_cast<const signedbv_typet &>(type);
1204 }
1205 
1210 {
1211  assert(type.id()==ID_signedbv);
1212  return static_cast<signedbv_typet &>(type);
1213 }
1214 
1218 {
1219 public:
1221  {
1222  }
1223 
1224  std::size_t get_fraction_bits() const
1225  {
1226  return get_width()-get_integer_bits();
1227  }
1228 
1229  std::size_t get_integer_bits() const;
1230 
1231  void set_integer_bits(std::size_t b)
1232  {
1233  set(ID_integer_bits, b);
1234  }
1235 };
1236 
1247 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
1248 {
1249  assert(type.id()==ID_fixedbv);
1250  return static_cast<const fixedbv_typet &>(type);
1251 }
1252 
1256 {
1257 public:
1259  {
1260  }
1261 
1262  std::size_t get_e() const
1263  {
1264  // subtract one for sign bit
1265  return get_width()-get_f()-1;
1266  }
1267 
1268  std::size_t get_f() const;
1269 
1270  void set_f(std::size_t b)
1271  {
1272  set(ID_f, b);
1273  }
1274 };
1275 
1286 inline const floatbv_typet &to_floatbv_type(const typet &type)
1287 {
1288  assert(type.id()==ID_floatbv);
1289  return static_cast<const floatbv_typet &>(type);
1290 }
1291 
1295 {
1296 public:
1298  {
1299  }
1300 
1301  explicit c_bit_field_typet(const typet &subtype, std::size_t width):
1302  bitvector_typet(ID_c_bit_field, subtype, width)
1303  {
1304  }
1305 
1306  // These have a sub-type
1307 };
1308 
1319 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
1320 {
1321  assert(type.id()==ID_c_bit_field);
1322  return static_cast<const c_bit_field_typet &>(type);
1323 }
1324 
1336 {
1337  assert(type.id()==ID_c_bit_field);
1338  return static_cast<c_bit_field_typet &>(type);
1339 }
1340 
1344 {
1345 public:
1347  {
1348  }
1349 
1350  // this one will go away; use the one with width
1351  explicit pointer_typet(const typet &_subtype):
1352  bitvector_typet(ID_pointer, _subtype)
1353  {
1354  }
1355 
1356  pointer_typet(const typet &_subtype, std::size_t width):
1357  bitvector_typet(ID_pointer, _subtype, width)
1358  {
1359  }
1360 
1362  {
1363  return signedbv_typet(get_width());
1364  }
1365 };
1366 
1377 inline const pointer_typet &to_pointer_type(const typet &type)
1378 {
1379  assert(type.id()==ID_pointer);
1380  return static_cast<const pointer_typet &>(type);
1381 }
1382 
1387 {
1388  assert(type.id()==ID_pointer);
1389  return static_cast<pointer_typet &>(type);
1390 }
1391 
1395 {
1396 public:
1398  {
1399  set(ID_C_reference, true);
1400  }
1401 
1402  // this one will go away; use the one with width
1403  explicit reference_typet(const typet &_subtype):
1404  pointer_typet(_subtype)
1405  {
1406  set(ID_C_reference, true);
1407  }
1408 
1409  reference_typet(const typet &_subtype, std::size_t _width):
1410  pointer_typet(_subtype, _width)
1411  {
1412  set(ID_C_reference, true);
1413  }
1414 };
1415 
1426 inline const reference_typet &to_reference_type(const typet &type)
1427 {
1428  assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1429  return static_cast<const reference_typet &>(type);
1430 }
1431 
1436 {
1437  assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1438  return static_cast<reference_typet &>(type);
1439 }
1440 
1443 bool is_reference(const typet &type);
1446 bool is_rvalue_reference(const typet &type);
1447 
1451 {
1452 public:
1454  {
1455  }
1456 
1457  explicit c_bool_typet(std::size_t width):
1458  bitvector_typet(ID_c_bool, width)
1459  {
1460  }
1461 };
1462 
1473 inline const c_bool_typet &to_c_bool_type(const typet &type)
1474 {
1475  assert(type.id()==ID_c_bool);
1476  return static_cast<const c_bool_typet &>(type);
1477 }
1478 
1483 {
1484  assert(type.id()==ID_c_bool);
1485  return static_cast<c_bool_typet &>(type);
1486 }
1487 
1490 class string_typet:public typet
1491 {
1492 public:
1493  string_typet():typet(ID_string)
1494  {
1495  }
1496 };
1497 
1508 inline const string_typet &to_string_type(const typet &type)
1509 {
1510  assert(type.id()==ID_string);
1511  return static_cast<const string_typet &>(type);
1512 }
1513 
1516 class range_typet:public typet
1517 {
1518 public:
1519  range_typet():typet(ID_range)
1520  {
1521  }
1522 
1523  range_typet(const mp_integer &_from, const mp_integer &_to)
1524  {
1525  set_from(_from);
1526  set_to(_to);
1527  }
1528 
1529  mp_integer get_from() const;
1530  mp_integer get_to() const;
1531 
1532  void set_from(const mp_integer &_from);
1533  void set_to(const mp_integer &to);
1534 };
1535 
1546 inline const range_typet &to_range_type(const typet &type)
1547 {
1548  assert(type.id()==ID_range);
1549  return static_cast<const range_typet &>(type);
1550 }
1551 
1555 {
1556 public:
1558  {
1559  }
1560 
1562  const typet &_subtype,
1563  const exprt &_size):type_with_subtypet(ID_vector, _subtype)
1564  {
1565  size()=_size;
1566  }
1567 
1568  const exprt &size() const
1569  {
1570  return static_cast<const exprt &>(find(ID_size));
1571  }
1572 
1574  {
1575  return static_cast<exprt &>(add(ID_size));
1576  }
1577 };
1578 
1589 inline const vector_typet &to_vector_type(const typet &type)
1590 {
1591  assert(type.id()==ID_vector);
1592  return static_cast<const vector_typet &>(type);
1593 }
1594 
1599 {
1600  assert(type.id()==ID_vector);
1601  return static_cast<vector_typet &>(type);
1602 }
1603 
1607 {
1608 public:
1610  {
1611  }
1612 
1613  explicit complex_typet(const typet &_subtype):
1614  type_with_subtypet(ID_complex, _subtype)
1615  {
1616  }
1617 };
1618 
1629 inline const complex_typet &to_complex_type(const typet &type)
1630 {
1631  assert(type.id()==ID_complex);
1632  return static_cast<const complex_typet &>(type);
1633 }
1634 
1639 {
1640  assert(type.id()==ID_complex);
1641  return static_cast<complex_typet &>(type);
1642 }
1643 
1644 #endif // CPROVER_UTIL_STD_TYPES_H
The void type.
Definition: std_types.h:63
const irept & get_nil_irep()
Definition: irep.cpp:56
const irep_idt & get_name() const
Definition: std_types.h:179
The type of an expression.
Definition: type.h:20
std::size_t get_e() const
Definition: std_types.h:1262
A generic tag-based type.
Definition: std_types.h:460
c_enum_typet(const typet &_subtype)
Definition: std_types.h:640
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
constant_exprt zero_expr() const
Definition: std_types.cpp:172
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
const irep_idt & get_identifier() const
Definition: std_types.h:479
array_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:908
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
bitvector_typet(const irep_idt &_id, const typet &_subtype, std::size_t width)
Definition: std_types.h:1015
bool is_rvalue_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:111
constant_exprt largest_expr() const
Definition: std_types.cpp:182
Natural numbers (which include zero)
Definition: std_types.h:79
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:1457
signedbv_typet(std::size_t width)
Definition: std_types.h:1178
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
std::vector< irept > subt
Definition: irep.h:91
irep_idt default_access() const
Definition: std_types.h:360
A generic enumeration type (not to be confused with C enums)
Definition: std_types.h:591
reference_typet(const typet &_subtype, std::size_t _width)
Definition: std_types.h:1409
bool has_base(const irep_idt &id) const
Definition: std_types.h:380
exprt & size()
Definition: std_types.h:1573
bool has_ellipsis() const
Definition: std_types.h:803
const tag_typet & to_tag_type(const typet &type)
Cast a generic typet to a tag_typet.
Definition: std_types.h:495
arrays without size
Definition: std_types.h:963
bool_typet()
Definition: std_types.h:36
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:194
void set_name(const irep_idt &name)
Definition: std_types.h:184
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
std::size_t get_integer_bits() const
Definition: std_types.cpp:15
pointer_typet(const typet &_subtype)
Definition: std_types.h:1351
Unbounded, signed rational numbers.
Definition: std_types.h:89
std::vector< componentt > componentst
Definition: std_types.h:240
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:1024
std::vector< parametert > parameterst
Definition: std_types.h:829
A union tag type.
Definition: std_types.h:554
const componentst & components() const
Definition: std_types.h:242
bool is_incomplete() const
Definition: std_types.h:930
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:157
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:121
A struct tag type.
Definition: std_types.h:517
const memberst & members() const
Definition: std_types.h:664
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
Definition: std_types.h:1546
typet & type()
Definition: expr.h:60
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:651
The proper Booleans.
Definition: std_types.h:33
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:474
unsignedbv_typet(std::size_t width)
Definition: std_types.h:1132
Type for c bit fields.
Definition: std_types.h:1294
bool has_default_value() const
Definition: std_types.h:759
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:1006
subt & get_sub()
Definition: irep.h:245
componentst & methods()
Definition: std_types.h:350
void set_base_name(const irep_idt &name)
Definition: std_types.h:777
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
irept::subt & bases()
Definition: std_types.h:370
const irep_idt & get_base_name() const
Definition: std_types.h:189
c_bit_field_typet(const typet &subtype, std::size_t width)
Definition: std_types.h:1301
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:162
mp_integer get_to() const
Definition: std_types.cpp:132
reference_typet(const typet &_subtype)
Definition: std_types.h:1403
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
void set_is_padding(bool is_padding)
Definition: std_types.h:234
exprt & size()
Definition: std_types.h:920
const irep_idt & get_base_name() const
Definition: std_types.h:787
std::vector< irep_idt > parameter_identifiers() const
Definition: std_types.h:862
void set_inlined(bool value)
Definition: std_types.h:856
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1473
const methodst & methods() const
Definition: std_types.h:345
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:680
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
void set_value(const irep_idt &value)
Definition: std_types.h:649
nil_typet()
Definition: std_types.h:46
void remove_ellipsis()
Definition: std_types.h:824
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
constant_exprt smallest_expr() const
Definition: std_types.cpp:152
A reference into the symbol table.
Definition: std_types.h:109
irep_idt get_identifier() const
Definition: std_types.h:650
The pointer type.
Definition: std_types.h:1343
symbol_typet(const irep_idt &identifier)
Definition: std_types.h:116
The empty type.
Definition: std_types.h:53
std::size_t get_fraction_bits() const
Definition: std_types.h:1224
void set_access(const irep_idt &access)
Definition: std_types.h:204
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
A constant-size array type.
Definition: std_types.h:1554
void set_integer_bits(std::size_t b)
Definition: std_types.h:1231
componentst & components()
Definition: std_types.h:247
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:1523
const exprt & size() const
Definition: std_types.h:1568
vector_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1561
void set_tag(const irep_idt &tag)
Definition: std_types.h:264
mp_integer smallest() const
Definition: std_types.cpp:162
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
const string_typet & to_string_type(const typet &type)
Cast a generic typet to a string_typet.
Definition: std_types.h:1508
void set_from(const mp_integer &_from)
Definition: std_types.cpp:117
signedbv_typet difference_type() const
Definition: std_types.h:1361
bv_typet(std::size_t width)
Definition: std_types.h:1092
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
mp_integer largest() const
Definition: std_types.cpp:167
mp_integer smallest() const
Definition: std_types.cpp:137
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
pointer_typet(const typet &_subtype, std::size_t width)
Definition: std_types.h:1356
bool get_this() const
Definition: std_types.h:792
complex_typet(const typet &_subtype)
Definition: std_types.h:1613
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1217
Base class of bitvector types.
Definition: std_types.h:1003
const irept::subt & elements() const
Definition: std_types.h:598
std::size_t get_width() const
Definition: std_types.h:1030
tag_typet(const irep_idt &_id)
Definition: std_types.h:463
const irep_idt & get_pretty_name() const
Definition: std_types.h:209
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:252
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
void make_ellipsis()
Definition: std_types.h:819
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1108
The reference type.
Definition: std_types.h:1394
componentt methodt
Definition: std_types.h:342
std::size_t get_f() const
Definition: std_types.cpp:22
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Definition: std_types.h:1426
Unbounded, signed integers.
Definition: std_types.h:69
Complex numbers made of pair of given subtype.
Definition: std_types.h:1606
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
typet & return_type()
Definition: std_types.h:836
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:772
mp_integer largest() const
Definition: std_types.cpp:142
bool is_prefix_of(const struct_typet &other) const
Definition: std_types.cpp:76
bool is_class() const
Definition: std_types.h:355
bool is_KnR() const
Definition: std_types.h:814
bitvector_typet(const irep_idt &_id, const typet &_subtype)
Definition: std_types.h:1010
constant_exprt largest_expr() const
Definition: std_types.cpp:157
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:536
const irep_idt & get_access() const
Definition: std_types.h:199
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
Unbounded, signed real numbers.
Definition: std_types.h:99
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
Definition: std_types.h:986
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:573
Base class for all expressions.
Definition: expr.h:46
const typet & find_type(const irep_namet &name) const
Definition: type.h:110
The union type.
Definition: std_types.h:424
const parameterst & parameters() const
Definition: std_types.h:841
exprt & default_value()
Definition: std_types.h:764
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
bool has_this() const
Definition: std_types.h:808
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:214
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
A type for subranges of integers.
Definition: std_types.h:1516
constant_exprt smallest_expr() const
Definition: std_types.cpp:177
irept & add(const irep_namet &name)
Definition: irep.cpp:306
typet & add_type(const irep_namet &name)
Definition: type.h:105
The NIL type.
Definition: std_types.h:43
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
bool is_complete() const
Definition: std_types.h:925
incomplete_array_typet(const typet &_subtype)
Definition: std_types.h:970
void set_f(std::size_t b)
Definition: std_types.h:1270
arrays with given size
Definition: std_types.h:901
void set_anonymous(bool anonymous)
Definition: std_types.h:224
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1629
irept::subt & elements()
Definition: std_types.h:603
const irept::subt & bases() const
Definition: std_types.h:365
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:520
exprt & add_expr(const irep_idt &name)
Definition: expr.h:152
void remove(const irep_namet &name)
Definition: irep.cpp:270
The C/C++ Booleans.
Definition: std_types.h:1450
const typet & subtype() const
Definition: type.h:31
irep_idt get_tag() const
Definition: std_types.h:263
C++ class type.
Definition: std_types.h:334
parametert(const typet &type)
Definition: std_types.h:750
bool get_inlined() const
Definition: std_types.h:851
parameterst & parameters()
Definition: std_types.h:846
void set_to(const mp_integer &to)
Definition: std_types.cpp:122
fixed-width bit-vector without numerical interpretation
Definition: std_types.h:1085
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
irep_idt get_base_name() const
Definition: std_types.h:655
c_enum_tag_typet(const irep_idt &identifier)
Definition: std_types.h:701
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
const irep_idt & get_identifier() const
Definition: std_types.h:782
std::vector< c_enum_membert > memberst
Definition: std_types.h:662
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
The type of C enums.
Definition: std_types.h:637
An enum tag type.
Definition: std_types.h:698
const typet & return_type() const
Definition: std_types.h:831
const irep_idt & get_identifier() const
Definition: std_types.h:126
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:656
void add_base(const typet &base)
Definition: std_types.h:375
const exprt & default_value() const
Definition: std_types.h:754
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
componentt(const irep_idt &_name, const typet &_type)
Definition: std_types.h:173
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
Definition: std_types.h:619
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
union_tag_typet(const irep_idt &identifier)
Definition: std_types.h:557
componentst methodst
Definition: std_types.h:343
void set_width(std::size_t width)
Definition: std_types.h:1035
irep_idt get_value() const
Definition: std_types.h:648
#define forall_irep(it, irep)
Definition: irep.h:62
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:407
constant_exprt zero_expr() const
Definition: std_types.cpp:147
mp_integer get_from() const
Definition: std_types.cpp:127
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051