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 #ifndef CPROVER_UTIL_STD_TYPES_H
10 #define CPROVER_UTIL_STD_TYPES_H
11 
19 #include "expr.h"
20 #include "mp_arith.h"
21 #include "invariant.h"
22 #include "expr_cast.h"
23 
24 #include <unordered_map>
25 
26 class constant_exprt;
27 
34 class bool_typet:public typet
35 {
36 public:
37  bool_typet():typet(ID_bool)
38  {
39  }
40 };
41 
44 class nil_typet:public typet
45 {
46 public:
47  nil_typet():typet(static_cast<const typet &>(get_nil_irep()))
48  {
49  }
50 };
51 
54 class empty_typet:public typet
55 {
56 public:
57  empty_typet():typet(ID_empty)
58  {
59  }
60 };
61 
64 class void_typet:public empty_typet
65 {
66 };
67 
70 class integer_typet:public typet
71 {
72 public:
73  integer_typet():typet(ID_integer)
74  {
75  }
76 };
77 
80 class natural_typet:public typet
81 {
82 public:
83  natural_typet():typet(ID_natural)
84  {
85  }
86 };
87 
90 class rational_typet:public typet
91 {
92 public:
93  rational_typet():typet(ID_rational)
94  {
95  }
96 };
97 
100 class real_typet:public typet
101 {
102 public:
103  real_typet():typet(ID_real)
104  {
105  }
106 };
107 
110 class symbol_typet:public typet
111 {
112 public:
113  explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
114  {
115  set_identifier(identifier);
116  }
117 
118  void set_identifier(const irep_idt &identifier)
119  {
120  set(ID_identifier, identifier);
121  }
122 
123  const irep_idt &get_identifier() const
124  {
125  return get(ID_identifier);
126  }
127 };
128 
139 inline const symbol_typet &to_symbol_type(const typet &type)
140 {
141  PRECONDITION(type.id()==ID_symbol);
142  return static_cast<const symbol_typet &>(type);
143 }
144 
149 {
150  PRECONDITION(type.id()==ID_symbol);
151  return static_cast<symbol_typet &>(type);
152 }
153 
154 template <>
155 inline bool can_cast_type<symbol_typet>(const typet &type)
156 {
157  return type.id() == ID_symbol;
158 }
159 
163 {
164 public:
165  explicit struct_union_typet(const irep_idt &_id):typet(_id)
166  {
167  }
168 
169  class componentt:public exprt
170  {
171  public:
173  {
174  }
175 
176  componentt(const irep_idt &_name, const typet &_type)
177  {
178  set_name(_name);
179  type()=_type;
180  }
181 
182  const irep_idt &get_name() const
183  {
184  return get(ID_name);
185  }
186 
187  void set_name(const irep_idt &name)
188  {
189  return set(ID_name, name);
190  }
191 
192  const irep_idt &get_base_name() const
193  {
194  return get(ID_base_name);
195  }
196 
197  void set_base_name(const irep_idt &base_name)
198  {
199  return set(ID_base_name, base_name);
200  }
201 
202  const irep_idt &get_access() const
203  {
204  return get(ID_access);
205  }
206 
207  void set_access(const irep_idt &access)
208  {
209  return set(ID_access, access);
210  }
211 
212  const irep_idt &get_pretty_name() const
213  {
214  return get(ID_pretty_name);
215  }
216 
217  void set_pretty_name(const irep_idt &name)
218  {
219  return set(ID_pretty_name, name);
220  }
221 
222  bool get_anonymous() const
223  {
224  return get_bool(ID_anonymous);
225  }
226 
227  void set_anonymous(bool anonymous)
228  {
229  return set(ID_anonymous, anonymous);
230  }
231 
232  bool get_is_padding() const
233  {
234  return get_bool(ID_C_is_padding);
235  }
236 
237  void set_is_padding(bool is_padding)
238  {
239  return set(ID_C_is_padding, is_padding);
240  }
241  };
242 
243  typedef std::vector<componentt> componentst;
244 
245  const componentst &components() const
246  {
247  return (const componentst &)(find(ID_components).get_sub());
248  }
249 
251  {
252  return (componentst &)(add(ID_components).get_sub());
253  }
254 
255  bool has_component(const irep_idt &component_name) const
256  {
257  return get_component(component_name).is_not_nil();
258  }
259 
260  const componentt &get_component(
261  const irep_idt &component_name) const;
262 
263  std::size_t component_number(const irep_idt &component_name) const;
264  typet component_type(const irep_idt &component_name) const;
265 
266  irep_idt get_tag() const { return get(ID_tag); }
267  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
268 };
269 
281 {
282  PRECONDITION(type.id()==ID_struct || type.id()==ID_union);
283  return static_cast<const struct_union_typet &>(type);
284 }
285 
290 {
291  PRECONDITION(type.id()==ID_struct || type.id()==ID_union);
292  return static_cast<struct_union_typet &>(type);
293 }
294 
298 {
299 public:
301  {
302  }
303 
304  // returns true if the object is a prefix of \a other
305  bool is_prefix_of(const struct_typet &other) const;
306 };
307 
318 inline const struct_typet &to_struct_type(const typet &type)
319 {
320  PRECONDITION(type.id()==ID_struct);
321  return static_cast<const struct_typet &>(type);
322 }
323 
328 {
329  PRECONDITION(type.id()==ID_struct);
330  return static_cast<struct_typet &>(type);
331 }
332 
333 template <>
334 inline bool can_cast_type<struct_typet>(const typet &type)
335 {
336  return type.id() == ID_struct;
337 }
338 
342 {
343 public:
345  {
346  set(ID_C_class, true);
347  }
348 
351 
352  const methodst &methods() const
353  {
354  return (const methodst &)(find(ID_methods).get_sub());
355  }
356 
358  {
359  return (methodst &)(add(ID_methods).get_sub());
360  }
361 
362  bool is_class() const
363  {
364  return get_bool(ID_C_class);
365  }
366 
368  {
369  return is_class()?ID_private:ID_public;
370  }
371 
372  class baset:public exprt
373  {
374  public:
375  baset():exprt(ID_base)
376  {
377  }
378 
379  explicit baset(const typet &base):exprt(ID_base, base)
380  {
381  }
382  };
383 
384  typedef std::vector<baset> basest;
385 
386  const basest &bases() const
387  {
388  return (const basest &)find(ID_bases).get_sub();
389  }
390 
392  {
393  return (basest &)add(ID_bases).get_sub();
394  }
395 
396  void add_base(const typet &base)
397  {
398  bases().push_back(baset(base));
399  }
400 
405  {
406  for(const auto &b : bases())
407  {
408  if(to_symbol_type(b.type()).get_identifier() == id)
409  return b;
410  }
411  return {};
412  }
413 
414  bool has_base(const irep_idt &id) const
415  {
416  return get_base(id).has_value();
417  }
418 
419  bool is_abstract() const
420  {
421  return get_bool(ID_abstract);
422  }
423 };
424 
435 inline const class_typet &to_class_type(const typet &type)
436 {
437  PRECONDITION(type.id()==ID_struct);
438  return static_cast<const class_typet &>(type);
439 }
440 
445 {
446  PRECONDITION(type.id()==ID_struct);
447  return static_cast<class_typet &>(type);
448 }
449 
450 template <>
451 inline bool can_cast_type<class_typet>(const typet &type)
452 {
453  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
454 }
455 
459 {
460 public:
462  {
463  }
464 };
465 
476 inline const union_typet &to_union_type(const typet &type)
477 {
478  PRECONDITION(type.id()==ID_union);
479  return static_cast<const union_typet &>(type);
480 }
481 
486 {
487  PRECONDITION(type.id()==ID_union);
488  return static_cast<union_typet &>(type);
489 }
490 
494 class tag_typet:public typet
495 {
496 public:
497  explicit tag_typet(
498  const irep_idt &_id,
499  const irep_idt &identifier):typet(_id)
500  {
501  set_identifier(identifier);
502  }
503 
504  void set_identifier(const irep_idt &identifier)
505  {
506  set(ID_identifier, identifier);
507  }
508 
509  const irep_idt &get_identifier() const
510  {
511  return get(ID_identifier);
512  }
513 };
514 
525 inline const tag_typet &to_tag_type(const typet &type)
526 {
527  PRECONDITION(type.id()==ID_c_enum_tag ||
528  type.id()==ID_struct_tag ||
529  type.id()==ID_union_tag);
530  return static_cast<const tag_typet &>(type);
531 }
532 
537 {
538  PRECONDITION(type.id()==ID_c_enum_tag ||
539  type.id()==ID_struct_tag ||
540  type.id()==ID_union_tag);
541  return static_cast<tag_typet &>(type);
542 }
543 
548 {
549 public:
550  explicit struct_tag_typet(const irep_idt &identifier):
551  tag_typet(ID_struct_tag, identifier)
552  {
553  }
554 };
555 
566 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
567 {
568  PRECONDITION(type.id()==ID_struct_tag);
569  return static_cast<const struct_tag_typet &>(type);
570 }
571 
576 {
577  PRECONDITION(type.id()==ID_struct_tag);
578  return static_cast<struct_tag_typet &>(type);
579 }
580 
585 {
586 public:
587  explicit union_tag_typet(const irep_idt &identifier):
588  tag_typet(ID_union_tag, identifier)
589  {
590  }
591 };
592 
603 inline const union_tag_typet &to_union_tag_type(const typet &type)
604 {
605  PRECONDITION(type.id()==ID_union_tag);
606  return static_cast<const union_tag_typet &>(type);
607 }
608 
613 {
614  PRECONDITION(type.id()==ID_union_tag);
615  return static_cast<union_tag_typet &>(type);
616 }
617 
622 {
623 public:
624  enumeration_typet():typet(ID_enumeration)
625  {
626  }
627 
628  const irept::subt &elements() const
629  {
630  return find(ID_elements).get_sub();
631  }
632 
634  {
635  return add(ID_elements).get_sub();
636  }
637 };
638 
649 inline const enumeration_typet &to_enumeration_type(const typet &type)
650 {
651  PRECONDITION(type.id()==ID_enumeration);
652  return static_cast<const enumeration_typet &>(type);
653 }
654 
659 {
660  PRECONDITION(type.id()==ID_enumeration);
661  return static_cast<enumeration_typet &>(type);
662 }
663 
668 {
669 public:
670  explicit c_enum_typet(const typet &_subtype):
671  type_with_subtypet(ID_c_enum, _subtype)
672  {
673  }
674 
675  class c_enum_membert:public irept
676  {
677  public:
678  irep_idt get_value() const { return get(ID_value); }
679  void set_value(const irep_idt &value) { set(ID_value, value); }
680  irep_idt get_identifier() const { return get(ID_identifier); }
681  void set_identifier(const irep_idt &identifier)
682  {
683  set(ID_identifier, identifier);
684  }
685  irep_idt get_base_name() const { return get(ID_base_name); }
686  void set_base_name(const irep_idt &base_name)
687  {
688  set(ID_base_name, base_name);
689  }
690  };
691 
692  typedef std::vector<c_enum_membert> memberst;
693 
694  const memberst &members() const
695  {
696  return (const memberst &)(find(ID_body).get_sub());
697  }
698 };
699 
710 inline const c_enum_typet &to_c_enum_type(const typet &type)
711 {
712  PRECONDITION(type.id()==ID_c_enum);
713  return static_cast<const c_enum_typet &>(type);
714 }
715 
720 {
721  PRECONDITION(type.id()==ID_c_enum);
722  return static_cast<c_enum_typet &>(type);
723 }
724 
729 {
730 public:
731  explicit c_enum_tag_typet(const irep_idt &identifier):
732  tag_typet(ID_c_enum_tag, identifier)
733  {
734  }
735 };
736 
747 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
748 {
749  PRECONDITION(type.id()==ID_c_enum_tag);
750  return static_cast<const c_enum_tag_typet &>(type);
751 }
752 
757 {
758  PRECONDITION(type.id()==ID_c_enum_tag);
759  return static_cast<c_enum_tag_typet &>(type);
760 }
761 
764 class code_typet:public typet
765 {
766 public:
767  class parametert;
768  typedef std::vector<parametert> parameterst;
769 
773  code_typet(parameterst &&_parameters, typet &&_return_type) : typet(ID_code)
774  {
775  parameters().swap(_parameters);
776  return_type().swap(_return_type);
777  }
778 
782  code_typet(parameterst &&_parameters, const typet &_return_type)
783  : typet(ID_code)
784  {
785  parameters().swap(_parameters);
786  return_type() = _return_type;
787  }
788 
790  DEPRECATED("Use the two argument constructor instead")
791  code_typet():typet(ID_code)
792  {
793  // make sure these properties are always there to avoid problems
794  // with irept comparisons
795  add(ID_parameters);
796  add_type(ID_return_type);
797  }
798 
799  // used to be argumentt -- now uses standard terminology
800 
801  class parametert:public exprt
802  {
803  public:
804  parametert():exprt(ID_parameter)
805  {
806  }
807 
808  explicit parametert(const typet &type):exprt(ID_parameter, type)
809  {
810  }
811 
812  const exprt &default_value() const
813  {
814  return find_expr(ID_C_default_value);
815  }
816 
817  bool has_default_value() const
818  {
819  return default_value().is_not_nil();
820  }
821 
823  {
824  return add_expr(ID_C_default_value);
825  }
826 
827  // The following for methods will go away;
828  // these should not be part of the signature of a function,
829  // but rather part of the body.
830  void set_identifier(const irep_idt &identifier)
831  {
832  set(ID_C_identifier, identifier);
833  }
834 
835  void set_base_name(const irep_idt &name)
836  {
837  set(ID_C_base_name, name);
838  }
839 
840  const irep_idt &get_identifier() const
841  {
842  return get(ID_C_identifier);
843  }
844 
845  const irep_idt &get_base_name() const
846  {
847  return get(ID_C_base_name);
848  }
849 
850  bool get_this() const
851  {
852  return get_bool(ID_C_this);
853  }
854 
855  void set_this()
856  {
857  set(ID_C_this, true);
858  }
859  };
860 
861  bool has_ellipsis() const
862  {
863  return find(ID_parameters).get_bool(ID_ellipsis);
864  }
865 
866  bool has_this() const
867  {
868  return get_this() != nullptr;
869  }
870 
871  const parametert *get_this() const
872  {
873  const parameterst &p=parameters();
874  if(!p.empty() && p.front().get_this())
875  return &p.front();
876  else
877  return nullptr;
878  }
879 
880  bool is_KnR() const
881  {
882  return get_bool(ID_C_KnR);
883  }
884 
886  {
887  add(ID_parameters).set(ID_ellipsis, true);
888  }
889 
891  {
892  add(ID_parameters).remove(ID_ellipsis);
893  }
894 
895  const typet &return_type() const
896  {
897  return find_type(ID_return_type);
898  }
899 
901  {
902  return add_type(ID_return_type);
903  }
904 
905  const parameterst &parameters() const
906  {
907  return (const parameterst &)find(ID_parameters).get_sub();
908  }
909 
911  {
912  return (parameterst &)add(ID_parameters).get_sub();
913  }
914 
915  bool get_inlined() const
916  {
917  return get_bool(ID_C_inlined);
918  }
919 
920  void set_inlined(bool value)
921  {
922  set(ID_C_inlined, value);
923  }
924 
925  const irep_idt &get_access() const
926  {
927  return get(ID_access);
928  }
929 
930  void set_access(const irep_idt &access)
931  {
932  return set(ID_access, access);
933  }
934 
935  bool get_is_constructor() const
936  {
937  return get_bool(ID_constructor);
938  }
939 
941  {
942  set(ID_constructor, true);
943  }
944 
945  // this produces the list of parameter identifiers
946  std::vector<irep_idt> parameter_identifiers() const
947  {
948  std::vector<irep_idt> result;
949  const parameterst &p=parameters();
950  result.reserve(p.size());
951  for(parameterst::const_iterator it=p.begin();
952  it!=p.end(); it++)
953  result.push_back(it->get_identifier());
954  return result;
955  }
956 
957  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
958 
961  {
963  const parameterst &p = parameters();
964  parameter_indices.reserve(p.size());
965  std::size_t index = 0;
966  for(const auto &p : parameters())
967  {
968  const irep_idt &id = p.get_identifier();
969  if(!id.empty())
970  parameter_indices.insert({ id, index });
971  ++index;
972  }
973  return parameter_indices;
974  }
975 };
976 
977 template <>
978 inline bool can_cast_type<code_typet>(const typet &type)
979 {
980  return type.id() == ID_code;
981 }
982 
993 inline const code_typet &to_code_type(const typet &type)
994 {
996  validate_type(type);
997  return static_cast<const code_typet &>(type);
998 }
999 
1004 {
1006  validate_type(type);
1007  return static_cast<code_typet &>(type);
1008 }
1009 
1010 
1014 {
1015 public:
1017  const typet &_subtype,
1018  const exprt &_size):type_with_subtypet(ID_array, _subtype)
1019  {
1020  size()=_size;
1021  }
1022 
1023  const exprt &size() const
1024  {
1025  return static_cast<const exprt &>(find(ID_size));
1026  }
1027 
1029  {
1030  return static_cast<exprt &>(add(ID_size));
1031  }
1032 
1033  bool is_complete() const
1034  {
1035  return size().is_not_nil();
1036  }
1037 
1038  bool is_incomplete() const
1039  {
1040  return size().is_nil();
1041  }
1042 };
1043 
1054 inline const array_typet &to_array_type(const typet &type)
1055 {
1056  PRECONDITION(type.id()==ID_array);
1057  return static_cast<const array_typet &>(type);
1058 }
1059 
1064 {
1065  PRECONDITION(type.id()==ID_array);
1066  return static_cast<array_typet &>(type);
1067 }
1068 
1072 {
1073 public:
1075  {
1076  }
1077 
1078  explicit incomplete_array_typet(const typet &_subtype):
1079  type_with_subtypet(ID_array, _subtype)
1080  {
1081  }
1082 };
1083 
1095 {
1096  PRECONDITION(type.id()==ID_array);
1097  return static_cast<const incomplete_array_typet &>(type);
1098 }
1099 
1104 {
1105  PRECONDITION(type.id()==ID_array);
1106  return static_cast<incomplete_array_typet &>(type);
1107 }
1108 
1112 {
1113 public:
1114  explicit bitvector_typet(const irep_idt &_id):type_with_subtypet(_id)
1115  {
1116  }
1117 
1118  bitvector_typet(const irep_idt &_id, const typet &_subtype):
1119  type_with_subtypet(_id, _subtype)
1120  {
1121  }
1122 
1124  const irep_idt &_id,
1125  const typet &_subtype,
1126  std::size_t width):
1127  type_with_subtypet(_id, _subtype)
1128  {
1129  set_width(width);
1130  }
1131 
1132  bitvector_typet(const irep_idt &_id, std::size_t width):
1133  type_with_subtypet(_id)
1134  {
1135  set_width(width);
1136  }
1137 
1138  std::size_t get_width() const
1139  {
1140  return get_size_t(ID_width);
1141  }
1142 
1143  void set_width(std::size_t width)
1144  {
1145  set(ID_width, width);
1146  }
1147 };
1148 
1159 inline const bitvector_typet &to_bitvector_type(const typet &type)
1160 {
1161  PRECONDITION(type.id()==ID_signedbv ||
1162  type.id()==ID_unsignedbv ||
1163  type.id()==ID_fixedbv ||
1164  type.id()==ID_floatbv ||
1165  type.id()==ID_verilog_signedbv ||
1166  type.id()==ID_verilog_unsignedbv ||
1167  type.id()==ID_bv ||
1168  type.id()==ID_pointer ||
1169  type.id()==ID_c_bit_field ||
1170  type.id()==ID_c_bool);
1171 
1172  return static_cast<const bitvector_typet &>(type);
1173 }
1174 
1176 {
1177  PRECONDITION(type.id()==ID_signedbv ||
1178  type.id()==ID_unsignedbv ||
1179  type.id()==ID_fixedbv ||
1180  type.id()==ID_floatbv ||
1181  type.id()==ID_verilog_signedbv ||
1182  type.id()==ID_verilog_unsignedbv ||
1183  type.id()==ID_bv ||
1184  type.id()==ID_pointer ||
1185  type.id()==ID_c_bit_field ||
1186  type.id()==ID_c_bool);
1187 
1188  return static_cast<bitvector_typet &>(type);
1189 }
1190 
1194 {
1195 public:
1196  explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
1197  {
1198  set_width(width);
1199  }
1200 };
1201 
1212 inline const bv_typet &to_bv_type(const typet &type)
1213 {
1214  PRECONDITION(type.id()==ID_bv);
1215  return static_cast<const bv_typet &>(type);
1216 }
1217 
1221 inline bv_typet &to_bv_type(typet &type)
1222 {
1223  PRECONDITION(type.id()==ID_bv);
1224  return static_cast<bv_typet &>(type);
1225 }
1226 
1230 {
1231 public:
1232  explicit unsignedbv_typet(std::size_t width):
1233  bitvector_typet(ID_unsignedbv, width)
1234  {
1235  }
1236 
1237  mp_integer smallest() const;
1238  mp_integer largest() const;
1239  constant_exprt smallest_expr() const;
1240  constant_exprt zero_expr() const;
1241  constant_exprt largest_expr() const;
1242 };
1243 
1254 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
1255 {
1256  PRECONDITION(type.id()==ID_unsignedbv);
1257  return static_cast<const unsignedbv_typet &>(type);
1258 }
1259 
1264 {
1265  PRECONDITION(type.id()==ID_unsignedbv);
1266  return static_cast<unsignedbv_typet &>(type);
1267 }
1268 
1272 {
1273 public:
1274  explicit signedbv_typet(std::size_t width):
1275  bitvector_typet(ID_signedbv, width)
1276  {
1277  }
1278 
1279  mp_integer smallest() const;
1280  mp_integer largest() const;
1281  constant_exprt smallest_expr() const;
1282  constant_exprt zero_expr() const;
1283  constant_exprt largest_expr() const;
1284 };
1285 
1296 inline const signedbv_typet &to_signedbv_type(const typet &type)
1297 {
1298  PRECONDITION(type.id()==ID_signedbv);
1299  return static_cast<const signedbv_typet &>(type);
1300 }
1301 
1306 {
1307  PRECONDITION(type.id()==ID_signedbv);
1308  return static_cast<signedbv_typet &>(type);
1309 }
1310 
1314 {
1315 public:
1317  {
1318  }
1319 
1320  std::size_t get_fraction_bits() const
1321  {
1322  return get_width()-get_integer_bits();
1323  }
1324 
1325  std::size_t get_integer_bits() const;
1326 
1327  void set_integer_bits(std::size_t b)
1328  {
1329  set(ID_integer_bits, b);
1330  }
1331 };
1332 
1343 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
1344 {
1345  PRECONDITION(type.id()==ID_fixedbv);
1346  return static_cast<const fixedbv_typet &>(type);
1347 }
1348 
1352 {
1353 public:
1355  {
1356  }
1357 
1358  std::size_t get_e() const
1359  {
1360  // subtract one for sign bit
1361  return get_width()-get_f()-1;
1362  }
1363 
1364  std::size_t get_f() const;
1365 
1366  void set_f(std::size_t b)
1367  {
1368  set(ID_f, b);
1369  }
1370 };
1371 
1382 inline const floatbv_typet &to_floatbv_type(const typet &type)
1383 {
1384  PRECONDITION(type.id()==ID_floatbv);
1385  return static_cast<const floatbv_typet &>(type);
1386 }
1387 
1391 {
1392 public:
1393  explicit c_bit_field_typet(const typet &subtype, std::size_t width):
1394  bitvector_typet(ID_c_bit_field, subtype, width)
1395  {
1396  }
1397 
1398  // These have a sub-type
1399 };
1400 
1411 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
1412 {
1413  PRECONDITION(type.id()==ID_c_bit_field);
1414  return static_cast<const c_bit_field_typet &>(type);
1415 }
1416 
1428 {
1429  PRECONDITION(type.id()==ID_c_bit_field);
1430  return static_cast<c_bit_field_typet &>(type);
1431 }
1432 
1436 {
1437 public:
1438  pointer_typet(const typet &_subtype, std::size_t width):
1439  bitvector_typet(ID_pointer, _subtype, width)
1440  {
1441  }
1442 
1444  {
1445  return signedbv_typet(get_width());
1446  }
1447 };
1448 
1459 inline const pointer_typet &to_pointer_type(const typet &type)
1460 {
1461  PRECONDITION(type.id()==ID_pointer);
1462  const pointer_typet &ret = static_cast<const pointer_typet &>(type);
1463  validate_type(ret);
1464  return ret;
1465 }
1466 
1471 {
1472  PRECONDITION(type.id()==ID_pointer);
1473  pointer_typet &ret = static_cast<pointer_typet &>(type);
1474  validate_type(ret);
1475  return ret;
1476 }
1477 
1478 template <>
1479 inline bool can_cast_type<pointer_typet>(const typet &type)
1480 {
1481  return type.id() == ID_pointer;
1482 }
1483 
1484 inline void validate_type(const pointer_typet &type)
1485 {
1486  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
1487  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
1488 }
1489 
1493 {
1494 public:
1495  reference_typet(const typet &_subtype, std::size_t _width):
1496  pointer_typet(_subtype, _width)
1497  {
1498  set(ID_C_reference, true);
1499  }
1500 };
1501 
1512 inline const reference_typet &to_reference_type(const typet &type)
1513 {
1514  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1515  PRECONDITION(!type.get(ID_width).empty());
1516  return static_cast<const reference_typet &>(type);
1517 }
1518 
1523 {
1524  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1525  PRECONDITION(!type.get(ID_width).empty());
1526  return static_cast<reference_typet &>(type);
1527 }
1528 
1531 bool is_reference(const typet &type);
1534 bool is_rvalue_reference(const typet &type);
1535 
1539 {
1540 public:
1542  {
1543  }
1544 
1545  explicit c_bool_typet(std::size_t width):
1546  bitvector_typet(ID_c_bool, width)
1547  {
1548  }
1549 };
1550 
1561 inline const c_bool_typet &to_c_bool_type(const typet &type)
1562 {
1563  PRECONDITION(type.id()==ID_c_bool);
1564  return static_cast<const c_bool_typet &>(type);
1565 }
1566 
1571 {
1572  PRECONDITION(type.id()==ID_c_bool);
1573  return static_cast<c_bool_typet &>(type);
1574 }
1575 
1578 class string_typet:public typet
1579 {
1580 public:
1581  string_typet():typet(ID_string)
1582  {
1583  }
1584 };
1585 
1596 inline const string_typet &to_string_type(const typet &type)
1597 {
1598  PRECONDITION(type.id()==ID_string);
1599  return static_cast<const string_typet &>(type);
1600 }
1601 
1604 class range_typet:public typet
1605 {
1606 public:
1607  range_typet(const mp_integer &_from, const mp_integer &_to)
1608  {
1609  set_from(_from);
1610  set_to(_to);
1611  }
1612 
1613  mp_integer get_from() const;
1614  mp_integer get_to() const;
1615 
1616  void set_from(const mp_integer &_from);
1617  void set_to(const mp_integer &to);
1618 };
1619 
1630 inline const range_typet &to_range_type(const typet &type)
1631 {
1632  PRECONDITION(type.id()==ID_range);
1633  return static_cast<const range_typet &>(type);
1634 }
1635 
1639 {
1640 public:
1642  const typet &_subtype,
1643  const exprt &_size):type_with_subtypet(ID_vector, _subtype)
1644  {
1645  size()=_size;
1646  }
1647 
1648  const exprt &size() const
1649  {
1650  return static_cast<const exprt &>(find(ID_size));
1651  }
1652 
1654  {
1655  return static_cast<exprt &>(add(ID_size));
1656  }
1657 };
1658 
1669 inline const vector_typet &to_vector_type(const typet &type)
1670 {
1671  PRECONDITION(type.id()==ID_vector);
1672  return static_cast<const vector_typet &>(type);
1673 }
1674 
1679 {
1680  PRECONDITION(type.id()==ID_vector);
1681  return static_cast<vector_typet &>(type);
1682 }
1683 
1687 {
1688 public:
1690  {
1691  }
1692 
1693  explicit complex_typet(const typet &_subtype):
1694  type_with_subtypet(ID_complex, _subtype)
1695  {
1696  }
1697 };
1698 
1709 inline const complex_typet &to_complex_type(const typet &type)
1710 {
1711  PRECONDITION(type.id()==ID_complex);
1712  return static_cast<const complex_typet &>(type);
1713 }
1714 
1719 {
1720  PRECONDITION(type.id()==ID_complex);
1721  return static_cast<complex_typet &>(type);
1722 }
1723 
1728 {
1729 public:
1730  // the domain of the function is composed of zero, one, or
1731  // many variables
1732  class variablet:public irept
1733  {
1734  public:
1735  // the identifier is optional
1737  {
1738  return get(ID_identifier);
1739  }
1740 
1741  void set_identifier(const irep_idt &identifier)
1742  {
1743  return set(ID_identifier, identifier);
1744  }
1745 
1747  {
1748  return static_cast<typet &>(add(ID_type));
1749  }
1750 
1751  const typet &type() const
1752  {
1753  return static_cast<const typet &>(find(ID_type));
1754  }
1755  };
1756 
1757  using domaint=std::vector<variablet>;
1758 
1759  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
1760  : typet(ID_mathematical_function)
1761  {
1762  subtypes().resize(2);
1763  domain() = _domain;
1764  codomain() = _codomain;
1765  }
1766 
1768  {
1769  return (domaint &)subtypes()[0].subtypes();
1770  }
1771 
1772  const domaint &domain() const
1773  {
1774  return (const domaint &)subtypes()[0].subtypes();
1775  }
1776 
1778  {
1779  auto &d=domain();
1780  d.push_back(variablet());
1781  return d.back();
1782  }
1783 
1784  // The codomain is the set of values that the
1785  // function maps to (the "target")
1787  {
1788  return subtypes()[1];
1789  }
1790 
1791  const typet &codomain() const
1792  {
1793  return subtypes()[1];
1794  }
1795 };
1796 
1807 inline const mathematical_function_typet &
1809 {
1810  PRECONDITION(type.id()==ID_mathematical_function);
1811  return static_cast<const mathematical_function_typet &>(type);
1812 }
1813 
1819 {
1820  PRECONDITION(type.id()==ID_mathematical_function);
1821  return static_cast<mathematical_function_typet &>(type);
1822 }
1823 
1824 #endif // CPROVER_UTIL_STD_TYPES_H
The void type.
Definition: std_types.h:64
const irept & get_nil_irep()
Definition: irep.cpp:56
bool can_cast_type< code_typet >(const typet &type)
Definition: std_types.h:978
const irep_idt & get_name() const
Definition: std_types.h:182
The type of an expression.
Definition: type.h:22
std::size_t get_e() const
Definition: std_types.h:1358
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
Definition: std_types.h:1759
A generic tag-based type.
Definition: std_types.h:494
c_enum_typet(const typet &_subtype)
Definition: std_types.h:670
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1229
constant_exprt zero_expr() const
Definition: std_types.cpp:172
void set_access(const irep_idt &access)
Definition: std_types.h:930
code_typet(parameterst &&_parameters, const typet &_return_type)
Constructs a new code type, i.e.
Definition: std_types.h:782
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
const irep_idt & get_identifier() const
Definition: std_types.h:509
array_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1016
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
bitvector_typet(const irep_idt &_id, const typet &_subtype, std::size_t width)
Definition: std_types.h:1123
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:80
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1296
std::vector< baset > basest
Definition: std_types.h:384
tag_typet(const irep_idt &_id, const irep_idt &identifier)
Definition: std_types.h:497
c_bool_typet(std::size_t width)
Definition: std_types.h:1545
signedbv_typet(std::size_t width)
Definition: std_types.h:1274
void validate_type(const pointer_typet &type)
Definition: std_types.h:1484
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Definition: std_types.h:1512
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1351
std::vector< irept > subt
Definition: irep.h:160
irep_idt default_access() const
Definition: std_types.h:367
A generic enumeration type (not to be confused with C enums)
Definition: std_types.h:621
reference_typet(const typet &_subtype, std::size_t _width)
Definition: std_types.h:1495
bool has_base(const irep_idt &id) const
Definition: std_types.h:414
exprt & size()
Definition: std_types.h:1653
bool has_ellipsis() const
Definition: std_types.h:861
arrays without size
Definition: std_types.h:1071
bool_typet()
Definition: std_types.h:37
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:197
void set_name(const irep_idt &name)
Definition: std_types.h:187
std::size_t get_integer_bits() const
Definition: std_types.cpp:15
const tag_typet & to_tag_type(const typet &type)
Cast a generic typet to a tag_typet.
Definition: std_types.h:525
Unbounded, signed rational numbers.
Definition: std_types.h:90
std::vector< componentt > componentst
Definition: std_types.h:243
subtypest & subtypes()
Definition: type.h:58
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:1132
std::vector< parametert > parameterst
Definition: std_types.h:767
std::vector< variablet > domaint
Definition: std_types.h:1757
A union tag type.
Definition: std_types.h:584
const componentst & components() const
Definition: std_types.h:245
bool is_incomplete() const
Definition: std_types.h:1038
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:140
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:118
A struct tag type.
Definition: std_types.h:547
const memberst & members() const
Definition: std_types.h:694
typet & type()
Definition: expr.h:56
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:681
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:435
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4422
Structure type.
Definition: std_types.h:297
bool get_is_constructor() const
Definition: std_types.h:935
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:504
unsignedbv_typet(std::size_t width)
Definition: std_types.h:1232
Type for c bit fields.
Definition: std_types.h:1390
bool has_default_value() const
Definition: std_types.h:817
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:1114
subt & get_sub()
Definition: irep.h:317
componentst & methods()
Definition: std_types.h:357
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1561
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
bool can_cast_type< pointer_typet >(const typet &type)
Definition: std_types.h:1479
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
Templated functions to cast to specific exprt-derived classes.
const irep_idt & get_base_name() const
Definition: std_types.h:192
c_bit_field_typet(const typet &subtype, std::size_t width)
Definition: std_types.h:1393
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:165
void set_is_constructor()
Definition: std_types.h:940
bool can_cast_type< struct_typet >(const typet &type)
Definition: std_types.h:334
mp_integer get_to() const
Definition: std_types.cpp:132
const irep_idt & id() const
Definition: irep.h:259
void set_is_padding(bool is_padding)
Definition: std_types.h:237
exprt & size()
Definition: std_types.h:1028
const irep_idt & get_base_name() const
Definition: std_types.h:845
std::vector< irep_idt > parameter_identifiers() const
Definition: std_types.h:946
void set_inlined(bool value)
Definition: std_types.h:920
const methodst & methods() const
Definition: std_types.h:352
void set_value(const irep_idt &value)
Definition: std_types.h:679
nil_typet()
Definition: std_types.h:47
void remove_ellipsis()
Definition: std_types.h:890
constant_exprt smallest_expr() const
Definition: std_types.cpp:152
A reference into the symbol table.
Definition: std_types.h:110
A type for mathematical functions (do not confuse with functions/methods in code) ...
Definition: std_types.h:1727
irep_idt get_identifier() const
Definition: std_types.h:680
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
Definition: std_types.h:649
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition: std_types.h:957
The pointer type.
Definition: std_types.h:1435
symbol_typet(const irep_idt &identifier)
Definition: std_types.h:113
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
The empty type.
Definition: std_types.h:54
std::size_t get_fraction_bits() const
Definition: std_types.h:1320
void set_access(const irep_idt &access)
Definition: std_types.h:207
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1271
const parametert * get_this() const
Definition: std_types.h:871
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:1741
A constant-size array type.
Definition: std_types.h:1638
nonstd::optional< T > optionalt
Definition: optional.h:35
void set_integer_bits(std::size_t b)
Definition: std_types.h:1327
componentst & components()
Definition: std_types.h:250
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:1607
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.h:404
const exprt & size() const
Definition: std_types.h:1648
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
vector_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1641
void set_tag(const irep_idt &tag)
Definition: std_types.h:267
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
mp_integer smallest() const
Definition: std_types.cpp:162
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1023
Base class for tree-like data structures with sharing.
Definition: irep.h:156
const domaint & domain() const
Definition: std_types.h:1772
void set_from(const mp_integer &_from)
Definition: std_types.cpp:117
signedbv_typet difference_type() const
Definition: std_types.h:1443
bv_typet(std::size_t width)
Definition: std_types.h:1196
mp_integer largest() const
Definition: std_types.cpp:167
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
mp_integer smallest() const
Definition: std_types.cpp:137
variablet & add_variable()
Definition: std_types.h:1777
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const irep_idt & get_access() const
Definition: std_types.h:925
pointer_typet(const typet &_subtype, std::size_t width)
Definition: std_types.h:1438
bool get_this() const
Definition: std_types.h:850
complex_typet(const typet &_subtype)
Definition: std_types.h:1693
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:1313
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1212
Base class of bitvector types.
Definition: std_types.h:1111
const irept::subt & elements() const
Definition: std_types.h:628
std::size_t get_width() const
Definition: std_types.h:1138
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:747
const irep_idt & get_pretty_name() const
Definition: std_types.h:212
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:255
void make_ellipsis()
Definition: std_types.h:885
const incomplete_array_typet & to_incomplete_array_type(const typet &type)
Cast a generic typet to an incomplete_array_typet.
Definition: std_types.h:1094
The reference type.
Definition: std_types.h:1492
componentt methodt
Definition: std_types.h:349
std::size_t get_f() const
Definition: std_types.cpp:22
#define DEPRECATED(msg)
Definition: deprecate.h:23
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1254
Unbounded, signed integers.
Definition: std_types.h:70
Complex numbers made of pair of given subtype.
Definition: std_types.h:1686
typet & return_type()
Definition: std_types.h:900
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:830
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:362
bool is_KnR() const
Definition: std_types.h:880
bitvector_typet(const irep_idt &_id, const typet &_subtype)
Definition: std_types.h:1118
constant_exprt largest_expr() const
Definition: std_types.cpp:157
const irep_idt & get_access() const
Definition: std_types.h:202
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
Unbounded, signed real numbers.
Definition: std_types.h:100
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition: std_types.h:960
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
const typet & find_type(const irep_namet &name) const
Definition: type.h:112
The union type.
Definition: std_types.h:458
const parameterst & parameters() const
Definition: std_types.h:905
exprt & default_value()
Definition: std_types.h:822
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
bool has_this() const
Definition: std_types.h:866
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:217
A type for subranges of integers.
Definition: std_types.h:1604
bool is_abstract() const
Definition: std_types.h:419
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
constant_exprt smallest_expr() const
Definition: std_types.cpp:177
baset(const typet &base)
Definition: std_types.h:379
const basest & bases() const
Definition: std_types.h:386
irept & add(const irep_namet &name)
Definition: irep.cpp:306
typet & add_type(const irep_namet &name)
Definition: type.h:107
The NIL type.
Definition: std_types.h:44
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1709
void swap(irept &irep)
Definition: irep.h:303
bool is_complete() const
Definition: std_types.h:1033
incomplete_array_typet(const typet &_subtype)
Definition: std_types.h:1078
void set_f(std::size_t b)
Definition: std_types.h:1366
arrays with given size
Definition: std_types.h:1013
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:1411
const string_typet & to_string_type(const typet &type)
Cast a generic typet to a string_typet.
Definition: std_types.h:1596
void set_anonymous(bool anonymous)
Definition: std_types.h:227
irept::subt & elements()
Definition: std_types.h:633
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:710
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
Definition: std_types.h:1630
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:550
exprt & add_expr(const irep_idt &name)
Definition: expr.h:135
void remove(const irep_namet &name)
Definition: irep.cpp:270
The C/C++ Booleans.
Definition: std_types.h:1538
const typet & subtype() const
Definition: type.h:33
irep_idt get_tag() const
Definition: std_types.h:266
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.
Definition: std_types.h:1808
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
C++ class type.
Definition: std_types.h:341
parametert(const typet &type)
Definition: std_types.h:808
bool get_inlined() const
Definition: std_types.h:915
parameterst & parameters()
Definition: std_types.h:910
void set_to(const mp_integer &to)
Definition: std_types.cpp:122
fixed-width bit-vector without numerical interpretation
Definition: std_types.h:1193
const typet & codomain() const
Definition: std_types.h:1791
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:685
c_enum_tag_typet(const irep_idt &identifier)
Definition: std_types.h:731
code_typet(parameterst &&_parameters, typet &&_return_type)
Constructs a new code type, i.e.
Definition: std_types.h:773
const irep_idt & get_identifier() const
Definition: std_types.h:840
std::vector< c_enum_membert > memberst
Definition: std_types.h:692
bool empty() const
Definition: dstring.h:73
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
The type of C enums.
Definition: std_types.h:667
An enum tag type.
Definition: std_types.h:728
bool can_cast_type< class_typet >(const typet &type)
Definition: std_types.h:451
const typet & return_type() const
Definition: std_types.h:895
bool can_cast_type< symbol_typet >(const typet &type)
Definition: std_types.h:155
const irep_idt & get_identifier() const
Definition: std_types.h:123
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:686
void add_base(const typet &base)
Definition: std_types.h:396
const exprt & default_value() const
Definition: std_types.h:812
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:176
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:587
componentst methodst
Definition: std_types.h:350
void set_width(std::size_t width)
Definition: std_types.h:1143
irep_idt get_value() const
Definition: std_types.h:678
basest & bases()
Definition: std_types.h:391
constant_exprt zero_expr() const
Definition: std_types.cpp:147
mp_integer get_from() const
Definition: std_types.cpp:127