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 
987 inline const code_typet &to_code_type(const typet &type)
988 {
989  PRECONDITION(type.id()==ID_code);
990  return static_cast<const code_typet &>(type);
991 }
992 
997 {
998  PRECONDITION(type.id()==ID_code);
999  return static_cast<code_typet &>(type);
1000 }
1001 
1005 {
1006 public:
1008  const typet &_subtype,
1009  const exprt &_size):type_with_subtypet(ID_array, _subtype)
1010  {
1011  size()=_size;
1012  }
1013 
1014  const exprt &size() const
1015  {
1016  return static_cast<const exprt &>(find(ID_size));
1017  }
1018 
1020  {
1021  return static_cast<exprt &>(add(ID_size));
1022  }
1023 
1024  bool is_complete() const
1025  {
1026  return size().is_not_nil();
1027  }
1028 
1029  bool is_incomplete() const
1030  {
1031  return size().is_nil();
1032  }
1033 };
1034 
1045 inline const array_typet &to_array_type(const typet &type)
1046 {
1047  PRECONDITION(type.id()==ID_array);
1048  return static_cast<const array_typet &>(type);
1049 }
1050 
1055 {
1056  PRECONDITION(type.id()==ID_array);
1057  return static_cast<array_typet &>(type);
1058 }
1059 
1063 {
1064 public:
1066  {
1067  }
1068 
1069  explicit incomplete_array_typet(const typet &_subtype):
1070  type_with_subtypet(ID_array, _subtype)
1071  {
1072  }
1073 };
1074 
1086 {
1087  PRECONDITION(type.id()==ID_array);
1088  return static_cast<const incomplete_array_typet &>(type);
1089 }
1090 
1095 {
1096  PRECONDITION(type.id()==ID_array);
1097  return static_cast<incomplete_array_typet &>(type);
1098 }
1099 
1103 {
1104 public:
1105  explicit bitvector_typet(const irep_idt &_id):type_with_subtypet(_id)
1106  {
1107  }
1108 
1109  bitvector_typet(const irep_idt &_id, const typet &_subtype):
1110  type_with_subtypet(_id, _subtype)
1111  {
1112  }
1113 
1115  const irep_idt &_id,
1116  const typet &_subtype,
1117  std::size_t width):
1118  type_with_subtypet(_id, _subtype)
1119  {
1120  set_width(width);
1121  }
1122 
1123  bitvector_typet(const irep_idt &_id, std::size_t width):
1124  type_with_subtypet(_id)
1125  {
1126  set_width(width);
1127  }
1128 
1129  std::size_t get_width() const
1130  {
1131  return get_size_t(ID_width);
1132  }
1133 
1134  void set_width(std::size_t width)
1135  {
1136  set(ID_width, width);
1137  }
1138 };
1139 
1150 inline const bitvector_typet &to_bitvector_type(const typet &type)
1151 {
1152  PRECONDITION(type.id()==ID_signedbv ||
1153  type.id()==ID_unsignedbv ||
1154  type.id()==ID_fixedbv ||
1155  type.id()==ID_floatbv ||
1156  type.id()==ID_verilog_signedbv ||
1157  type.id()==ID_verilog_unsignedbv ||
1158  type.id()==ID_bv ||
1159  type.id()==ID_pointer ||
1160  type.id()==ID_c_bit_field ||
1161  type.id()==ID_c_bool);
1162 
1163  return static_cast<const bitvector_typet &>(type);
1164 }
1165 
1167 {
1168  PRECONDITION(type.id()==ID_signedbv ||
1169  type.id()==ID_unsignedbv ||
1170  type.id()==ID_fixedbv ||
1171  type.id()==ID_floatbv ||
1172  type.id()==ID_verilog_signedbv ||
1173  type.id()==ID_verilog_unsignedbv ||
1174  type.id()==ID_bv ||
1175  type.id()==ID_pointer ||
1176  type.id()==ID_c_bit_field ||
1177  type.id()==ID_c_bool);
1178 
1179  return static_cast<bitvector_typet &>(type);
1180 }
1181 
1185 {
1186 public:
1187  explicit bv_typet(std::size_t width):bitvector_typet(ID_bv)
1188  {
1189  set_width(width);
1190  }
1191 };
1192 
1203 inline const bv_typet &to_bv_type(const typet &type)
1204 {
1205  PRECONDITION(type.id()==ID_bv);
1206  return static_cast<const bv_typet &>(type);
1207 }
1208 
1212 inline bv_typet &to_bv_type(typet &type)
1213 {
1214  PRECONDITION(type.id()==ID_bv);
1215  return static_cast<bv_typet &>(type);
1216 }
1217 
1221 {
1222 public:
1223  explicit unsignedbv_typet(std::size_t width):
1224  bitvector_typet(ID_unsignedbv, width)
1225  {
1226  }
1227 
1228  mp_integer smallest() const;
1229  mp_integer largest() const;
1230  constant_exprt smallest_expr() const;
1231  constant_exprt zero_expr() const;
1232  constant_exprt largest_expr() const;
1233 };
1234 
1245 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
1246 {
1247  PRECONDITION(type.id()==ID_unsignedbv);
1248  return static_cast<const unsignedbv_typet &>(type);
1249 }
1250 
1255 {
1256  PRECONDITION(type.id()==ID_unsignedbv);
1257  return static_cast<unsignedbv_typet &>(type);
1258 }
1259 
1263 {
1264 public:
1265  explicit signedbv_typet(std::size_t width):
1266  bitvector_typet(ID_signedbv, width)
1267  {
1268  }
1269 
1270  mp_integer smallest() const;
1271  mp_integer largest() const;
1272  constant_exprt smallest_expr() const;
1273  constant_exprt zero_expr() const;
1274  constant_exprt largest_expr() const;
1275 };
1276 
1287 inline const signedbv_typet &to_signedbv_type(const typet &type)
1288 {
1289  PRECONDITION(type.id()==ID_signedbv);
1290  return static_cast<const signedbv_typet &>(type);
1291 }
1292 
1297 {
1298  PRECONDITION(type.id()==ID_signedbv);
1299  return static_cast<signedbv_typet &>(type);
1300 }
1301 
1305 {
1306 public:
1308  {
1309  }
1310 
1311  std::size_t get_fraction_bits() const
1312  {
1313  return get_width()-get_integer_bits();
1314  }
1315 
1316  std::size_t get_integer_bits() const;
1317 
1318  void set_integer_bits(std::size_t b)
1319  {
1320  set(ID_integer_bits, b);
1321  }
1322 };
1323 
1334 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
1335 {
1336  PRECONDITION(type.id()==ID_fixedbv);
1337  return static_cast<const fixedbv_typet &>(type);
1338 }
1339 
1343 {
1344 public:
1346  {
1347  }
1348 
1349  std::size_t get_e() const
1350  {
1351  // subtract one for sign bit
1352  return get_width()-get_f()-1;
1353  }
1354 
1355  std::size_t get_f() const;
1356 
1357  void set_f(std::size_t b)
1358  {
1359  set(ID_f, b);
1360  }
1361 };
1362 
1373 inline const floatbv_typet &to_floatbv_type(const typet &type)
1374 {
1375  PRECONDITION(type.id()==ID_floatbv);
1376  return static_cast<const floatbv_typet &>(type);
1377 }
1378 
1382 {
1383 public:
1384  explicit c_bit_field_typet(const typet &subtype, std::size_t width):
1385  bitvector_typet(ID_c_bit_field, subtype, width)
1386  {
1387  }
1388 
1389  // These have a sub-type
1390 };
1391 
1402 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
1403 {
1404  PRECONDITION(type.id()==ID_c_bit_field);
1405  return static_cast<const c_bit_field_typet &>(type);
1406 }
1407 
1419 {
1420  PRECONDITION(type.id()==ID_c_bit_field);
1421  return static_cast<c_bit_field_typet &>(type);
1422 }
1423 
1427 {
1428 public:
1429  pointer_typet(const typet &_subtype, std::size_t width):
1430  bitvector_typet(ID_pointer, _subtype, width)
1431  {
1432  }
1433 
1435  {
1436  return signedbv_typet(get_width());
1437  }
1438 };
1439 
1450 inline const pointer_typet &to_pointer_type(const typet &type)
1451 {
1452  PRECONDITION(type.id()==ID_pointer);
1453  const pointer_typet &ret = static_cast<const pointer_typet &>(type);
1454  validate_type(ret);
1455  return ret;
1456 }
1457 
1462 {
1463  PRECONDITION(type.id()==ID_pointer);
1464  pointer_typet &ret = static_cast<pointer_typet &>(type);
1465  validate_type(ret);
1466  return ret;
1467 }
1468 
1469 template <>
1470 inline bool can_cast_type<pointer_typet>(const typet &type)
1471 {
1472  return type.id() == ID_pointer;
1473 }
1474 
1475 inline void validate_type(const pointer_typet &type)
1476 {
1477  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
1478  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
1479 }
1480 
1484 {
1485 public:
1486  reference_typet(const typet &_subtype, std::size_t _width):
1487  pointer_typet(_subtype, _width)
1488  {
1489  set(ID_C_reference, true);
1490  }
1491 };
1492 
1503 inline const reference_typet &to_reference_type(const typet &type)
1504 {
1505  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1506  PRECONDITION(!type.get(ID_width).empty());
1507  return static_cast<const reference_typet &>(type);
1508 }
1509 
1514 {
1515  PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1516  PRECONDITION(!type.get(ID_width).empty());
1517  return static_cast<reference_typet &>(type);
1518 }
1519 
1522 bool is_reference(const typet &type);
1525 bool is_rvalue_reference(const typet &type);
1526 
1530 {
1531 public:
1533  {
1534  }
1535 
1536  explicit c_bool_typet(std::size_t width):
1537  bitvector_typet(ID_c_bool, width)
1538  {
1539  }
1540 };
1541 
1552 inline const c_bool_typet &to_c_bool_type(const typet &type)
1553 {
1554  PRECONDITION(type.id()==ID_c_bool);
1555  return static_cast<const c_bool_typet &>(type);
1556 }
1557 
1562 {
1563  PRECONDITION(type.id()==ID_c_bool);
1564  return static_cast<c_bool_typet &>(type);
1565 }
1566 
1569 class string_typet:public typet
1570 {
1571 public:
1572  string_typet():typet(ID_string)
1573  {
1574  }
1575 };
1576 
1587 inline const string_typet &to_string_type(const typet &type)
1588 {
1589  PRECONDITION(type.id()==ID_string);
1590  return static_cast<const string_typet &>(type);
1591 }
1592 
1595 class range_typet:public typet
1596 {
1597 public:
1598  range_typet(const mp_integer &_from, const mp_integer &_to)
1599  {
1600  set_from(_from);
1601  set_to(_to);
1602  }
1603 
1604  mp_integer get_from() const;
1605  mp_integer get_to() const;
1606 
1607  void set_from(const mp_integer &_from);
1608  void set_to(const mp_integer &to);
1609 };
1610 
1621 inline const range_typet &to_range_type(const typet &type)
1622 {
1623  PRECONDITION(type.id()==ID_range);
1624  return static_cast<const range_typet &>(type);
1625 }
1626 
1630 {
1631 public:
1633  const typet &_subtype,
1634  const exprt &_size):type_with_subtypet(ID_vector, _subtype)
1635  {
1636  size()=_size;
1637  }
1638 
1639  const exprt &size() const
1640  {
1641  return static_cast<const exprt &>(find(ID_size));
1642  }
1643 
1645  {
1646  return static_cast<exprt &>(add(ID_size));
1647  }
1648 };
1649 
1660 inline const vector_typet &to_vector_type(const typet &type)
1661 {
1662  PRECONDITION(type.id()==ID_vector);
1663  return static_cast<const vector_typet &>(type);
1664 }
1665 
1670 {
1671  PRECONDITION(type.id()==ID_vector);
1672  return static_cast<vector_typet &>(type);
1673 }
1674 
1678 {
1679 public:
1681  {
1682  }
1683 
1684  explicit complex_typet(const typet &_subtype):
1685  type_with_subtypet(ID_complex, _subtype)
1686  {
1687  }
1688 };
1689 
1700 inline const complex_typet &to_complex_type(const typet &type)
1701 {
1702  PRECONDITION(type.id()==ID_complex);
1703  return static_cast<const complex_typet &>(type);
1704 }
1705 
1710 {
1711  PRECONDITION(type.id()==ID_complex);
1712  return static_cast<complex_typet &>(type);
1713 }
1714 
1719 {
1720 public:
1721  // the domain of the function is composed of zero, one, or
1722  // many variables
1723  class variablet:public irept
1724  {
1725  public:
1726  // the identifier is optional
1728  {
1729  return get(ID_identifier);
1730  }
1731 
1732  void set_identifier(const irep_idt &identifier)
1733  {
1734  return set(ID_identifier, identifier);
1735  }
1736 
1738  {
1739  return static_cast<typet &>(add(ID_type));
1740  }
1741 
1742  const typet &type() const
1743  {
1744  return static_cast<const typet &>(find(ID_type));
1745  }
1746  };
1747 
1748  using domaint=std::vector<variablet>;
1749 
1750  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
1751  : typet(ID_mathematical_function)
1752  {
1753  subtypes().resize(2);
1754  domain() = _domain;
1755  codomain() = _codomain;
1756  }
1757 
1759  {
1760  return (domaint &)subtypes()[0].subtypes();
1761  }
1762 
1763  const domaint &domain() const
1764  {
1765  return (const domaint &)subtypes()[0].subtypes();
1766  }
1767 
1769  {
1770  auto &d=domain();
1771  d.push_back(variablet());
1772  return d.back();
1773  }
1774 
1775  // The codomain is the set of values that the
1776  // function maps to (the "target")
1778  {
1779  return subtypes()[1];
1780  }
1781 
1782  const typet &codomain() const
1783  {
1784  return subtypes()[1];
1785  }
1786 };
1787 
1798 inline const mathematical_function_typet &
1800 {
1801  PRECONDITION(type.id()==ID_mathematical_function);
1802  return static_cast<const mathematical_function_typet &>(type);
1803 }
1804 
1810 {
1811  PRECONDITION(type.id()==ID_mathematical_function);
1812  return static_cast<mathematical_function_typet &>(type);
1813 }
1814 
1815 #endif // CPROVER_UTIL_STD_TYPES_H
The void type.
Definition: std_types.h:64
const irept & get_nil_irep()
Definition: irep.cpp:56
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:1349
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
Definition: std_types.h:1750
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:1220
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:1007
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
bitvector_typet(const irep_idt &_id, const typet &_subtype, std::size_t width)
Definition: std_types.h:1114
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:1287
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:1536
signedbv_typet(std::size_t width)
Definition: std_types.h:1265
void validate_type(const pointer_typet &type)
Definition: std_types.h:1475
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Definition: std_types.h:1503
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1342
std::vector< irept > subt
Definition: irep.h:90
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:1486
bool has_base(const irep_idt &id) const
Definition: std_types.h:414
exprt & size()
Definition: std_types.h:1644
bool has_ellipsis() const
Definition: std_types.h:861
arrays without size
Definition: std_types.h:1062
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:987
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:1123
std::vector< parametert > parameterst
Definition: std_types.h:767
std::vector< variablet > domaint
Definition: std_types.h:1748
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:1029
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:4424
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:1223
Type for c bit fields.
Definition: std_types.h:1381
bool has_default_value() const
Definition: std_types.h:817
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:1105
subt & get_sub()
Definition: irep.h:245
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:1552
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:1470
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
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:1384
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:189
void set_is_padding(bool is_padding)
Definition: std_types.h:237
exprt & size()
Definition: std_types.h:1019
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:1718
irep_idt get_identifier() const
Definition: std_types.h:680
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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:1426
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:1311
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:1262
const parametert * get_this() const
Definition: std_types.h:871
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:1732
A constant-size array type.
Definition: std_types.h:1629
nonstd::optional< T > optionalt
Definition: optional.h:35
void set_integer_bits(std::size_t b)
Definition: std_types.h:1318
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:1598
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:1639
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
vector_typet(const typet &_subtype, const exprt &_size)
Definition: std_types.h:1632
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:1660
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 union_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1014
Base class for tree-like data structures with sharing.
Definition: irep.h:86
const domaint & domain() const
Definition: std_types.h:1763
void set_from(const mp_integer &_from)
Definition: std_types.cpp:117
signedbv_typet difference_type() const
Definition: std_types.h:1434
bv_typet(std::size_t width)
Definition: std_types.h:1187
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:1768
const irep_idt & get_access() const
Definition: std_types.h:925
pointer_typet(const typet &_subtype, std::size_t width)
Definition: std_types.h:1429
bool get_this() const
Definition: std_types.h:850
complex_typet(const typet &_subtype)
Definition: std_types.h:1684
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:1304
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1203
Base class of bitvector types.
Definition: std_types.h:1102
const irept::subt & elements() const
Definition: std_types.h:628
std::size_t get_width() const
Definition: std_types.h:1129
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:1085
The reference type.
Definition: std_types.h:1483
componentt methodt
Definition: std_types.h:349
std::size_t get_f() const
Definition: std_types.cpp:22
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
Unbounded, signed integers.
Definition: std_types.h:70
Complex numbers made of pair of given subtype.
Definition: std_types.h:1677
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:1109
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:1373
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:1334
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:1045
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:1595
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:1700
void swap(irept &irep)
Definition: irep.h:231
bool is_complete() const
Definition: std_types.h:1024
incomplete_array_typet(const typet &_subtype)
Definition: std_types.h:1069
void set_f(std::size_t b)
Definition: std_types.h:1357
arrays with given size
Definition: std_types.h:1004
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:1402
const string_typet & to_string_type(const typet &type)
Cast a generic typet to a string_typet.
Definition: std_types.h:1587
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:1450
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:1621
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:1529
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:1799
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
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:1184
const typet & codomain() const
Definition: std_types.h:1782
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:61
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:214
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:1134
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