CBMC
std_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pre-defined types
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_STD_TYPES_H
14 #define CPROVER_UTIL_STD_TYPES_H
15 
16 #include "expr.h"
17 #include "expr_cast.h" // IWYU pragma: keep
18 #include "invariant.h"
19 #include "mp_arith.h"
20 #include "validate.h"
21 
22 #include <unordered_map>
23 
24 class constant_exprt;
25 class namespacet;
26 
29 inline bool is_constant(const typet &type)
30 {
31  return type.get_bool(ID_C_constant);
32 }
33 
35 class bool_typet:public typet
36 {
37 public:
38  bool_typet():typet(ID_bool)
39  {
40  }
41 };
42 
43 template <>
44 inline bool can_cast_type<bool_typet>(const typet &base)
45 {
46  return base.id() == ID_bool;
47 }
48 
50 class empty_typet:public typet
51 {
52 public:
53  empty_typet():typet(ID_empty)
54  {
55  }
56 };
57 
62 {
63 public:
64  explicit struct_union_typet(const irep_idt &_id):typet(_id)
65  {
66  }
67 
68  class componentt:public exprt
69  {
70  public:
71  componentt() = default;
72 
73  componentt(const irep_idt &_name, typet _type)
74  {
75  set_name(_name);
76  type().swap(_type);
77  }
78 
79  const irep_idt &get_name() const
80  {
81  return get(ID_name);
82  }
83 
84  void set_name(const irep_idt &name)
85  {
86  return set(ID_name, name);
87  }
88 
89  const irep_idt &get_base_name() const
90  {
91  return get(ID_base_name);
92  }
93 
94  void set_base_name(const irep_idt &base_name)
95  {
96  return set(ID_base_name, base_name);
97  }
98 
99  const irep_idt &get_access() const
100  {
101  return get(ID_access);
102  }
103 
104  void set_access(const irep_idt &access)
105  {
106  return set(ID_access, access);
107  }
108 
109  const irep_idt &get_pretty_name() const
110  {
111  return get(ID_pretty_name);
112  }
113 
114  void set_pretty_name(const irep_idt &name)
115  {
116  return set(ID_pretty_name, name);
117  }
118 
119  bool get_anonymous() const
120  {
121  return get_bool(ID_anonymous);
122  }
123 
124  void set_anonymous(bool anonymous)
125  {
126  return set(ID_anonymous, anonymous);
127  }
128 
129  bool get_is_padding() const
130  {
131  return get_bool(ID_C_is_padding);
132  }
133 
134  void set_is_padding(bool is_padding)
135  {
136  return set(ID_C_is_padding, is_padding);
137  }
138  };
139 
140  typedef std::vector<componentt> componentst;
141 
142  struct_union_typet(const irep_idt &_id, componentst _components) : typet(_id)
143  {
144  components() = std::move(_components);
145  }
146 
147  const componentst &components() const
148  {
149  return (const componentst &)(find(ID_components).get_sub());
150  }
151 
153  {
154  return (componentst &)(add(ID_components).get_sub());
155  }
156 
157  bool has_component(const irep_idt &component_name) const
158  {
159  return get_component(component_name).is_not_nil();
160  }
161 
162  const componentt &get_component(
163  const irep_idt &component_name) const;
164 
165  std::size_t component_number(const irep_idt &component_name) const;
166  const typet &component_type(const irep_idt &component_name) const;
167 
168  irep_idt get_tag() const { return get(ID_tag); }
169  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
170 
172  bool is_class() const
173  {
174  return id() == ID_struct && get_bool(ID_C_class);
175  }
176 
180  {
181  return is_class() ? ID_private : ID_public;
182  }
183 
185  bool is_incomplete() const
186  {
187  return get_bool(ID_incomplete);
188  }
189 
192  {
193  set(ID_incomplete, true);
194  }
195 };
196 
200 template <>
201 inline bool can_cast_type<struct_union_typet>(const typet &type)
202 {
203  return type.id() == ID_struct || type.id() == ID_union;
204 }
205 
215 {
217  return static_cast<const struct_union_typet &>(type);
218 }
219 
222 {
224  return static_cast<struct_union_typet &>(type);
225 }
226 
227 class struct_tag_typet;
228 
231 {
232 public:
234  {
235  }
236 
237  explicit struct_typet(componentst _components)
238  : struct_union_typet(ID_struct, std::move(_components))
239  {
240  }
241 
242  bool is_prefix_of(const struct_typet &other) const;
243 
245  bool is_class() const
246  {
247  return get_bool(ID_C_class);
248  }
249 
251  class baset : public exprt
252  {
253  public:
255  const struct_tag_typet &type() const;
256  explicit baset(struct_tag_typet base);
257  };
258 
259  typedef std::vector<baset> basest;
260 
262  const basest &bases() const
263  {
264  return (const basest &)find(ID_bases).get_sub();
265  }
266 
269  {
270  return (basest &)add(ID_bases).get_sub();
271  }
272 
275  void add_base(const struct_tag_typet &base);
276 
280  optionalt<baset> get_base(const irep_idt &id) const;
281 
285  bool has_base(const irep_idt &id) const
286  {
287  return get_base(id).has_value();
288  }
289 };
290 
294 template <>
295 inline bool can_cast_type<struct_typet>(const typet &type)
296 {
297  return type.id() == ID_struct;
298 }
299 
308 inline const struct_typet &to_struct_type(const typet &type)
309 {
311  return static_cast<const struct_typet &>(type);
312 }
313 
316 {
318  return static_cast<struct_typet &>(type);
319 }
320 
325 {
326 public:
328  {
329  set(ID_C_class, true);
330  }
331 
332  typedef componentt methodt;
334 
335  const methodst &methods() const
336  {
337  return (const methodst &)(find(ID_methods).get_sub());
338  }
339 
341  {
342  return (methodst &)(add(ID_methods).get_sub());
343  }
344 
345  using static_membert = componentt;
347 
349  {
350  return (const static_memberst &)(find(ID_static_members).get_sub());
351  }
352 
354  {
355  return (static_memberst &)(add(ID_static_members).get_sub());
356  }
357 
358  bool is_abstract() const
359  {
360  return get_bool(ID_abstract);
361  }
362 };
363 
367 template <>
368 inline bool can_cast_type<class_typet>(const typet &type)
369 {
370  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
371 }
372 
381 inline const class_typet &to_class_type(const typet &type)
382 {
384  return static_cast<const class_typet &>(type);
385 }
386 
389 {
391  return static_cast<class_typet &>(type);
392 }
393 
395 class tag_typet:public typet
396 {
397 public:
398  explicit tag_typet(
399  const irep_idt &_id,
400  const irep_idt &identifier):typet(_id)
401  {
402  set_identifier(identifier);
403  }
404 
405  void set_identifier(const irep_idt &identifier)
406  {
407  set(ID_identifier, identifier);
408  }
409 
410  const irep_idt &get_identifier() const
411  {
412  return get(ID_identifier);
413  }
414 };
415 
419 template <>
420 inline bool can_cast_type<tag_typet>(const typet &type)
421 {
422  return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
423  type.id() == ID_union_tag;
424 }
425 
434 inline const tag_typet &to_tag_type(const typet &type)
435 {
437  return static_cast<const tag_typet &>(type);
438 }
439 
442 {
444  return static_cast<tag_typet &>(type);
445 }
446 
449 {
450 public:
451  explicit struct_tag_typet(const irep_idt &identifier):
452  tag_typet(ID_struct_tag, identifier)
453  {
454  }
455 };
456 
460 template <>
461 inline bool can_cast_type<struct_tag_typet>(const typet &type)
462 {
463  return type.id() == ID_struct_tag;
464 }
465 
474 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
475 {
477  return static_cast<const struct_tag_typet &>(type);
478 }
479 
482 {
484  return static_cast<struct_tag_typet &>(type);
485 }
486 
490 {
491 public:
492  enumeration_typet():typet(ID_enumeration)
493  {
494  }
495 
496  const irept::subt &elements() const
497  {
498  return find(ID_elements).get_sub();
499  }
500 
502  {
503  return add(ID_elements).get_sub();
504  }
505 };
506 
510 template <>
511 inline bool can_cast_type<enumeration_typet>(const typet &type)
512 {
513  return type.id() == ID_enumeration;
514 }
515 
524 inline const enumeration_typet &to_enumeration_type(const typet &type)
525 {
527  return static_cast<const enumeration_typet &>(type);
528 }
529 
532 {
534  return static_cast<enumeration_typet &>(type);
535 }
536 
538 class code_typet:public typet
539 {
540 public:
541  class parametert;
542  typedef std::vector<parametert> parameterst;
543 
547  code_typet(parameterst _parameters, typet _return_type) : typet(ID_code)
548  {
549  parameters().swap(_parameters);
550  return_type().swap(_return_type);
551  }
552 
553  // used to be argumentt -- now uses standard terminology
554 
555  class parametert:public exprt
556  {
557  public:
558  explicit parametert(const typet &type):exprt(ID_parameter, type)
559  {
560  }
561 
562  const exprt &default_value() const
563  {
564  return find_expr(ID_C_default_value);
565  }
566 
567  bool has_default_value() const
568  {
569  return default_value().is_not_nil();
570  }
571 
573  {
574  return add_expr(ID_C_default_value);
575  }
576 
577  // The following for methods will go away;
578  // these should not be part of the signature of a function,
579  // but rather part of the body.
580  void set_identifier(const irep_idt &identifier)
581  {
582  set(ID_C_identifier, identifier);
583  }
584 
585  void set_base_name(const irep_idt &name)
586  {
587  set(ID_C_base_name, name);
588  }
589 
590  const irep_idt &get_identifier() const
591  {
592  return get(ID_C_identifier);
593  }
594 
595  const irep_idt &get_base_name() const
596  {
597  return get(ID_C_base_name);
598  }
599 
600  bool get_this() const
601  {
602  return get_bool(ID_C_this);
603  }
604 
605  void set_this()
606  {
607  set(ID_C_this, true);
608  }
609  };
610 
611  bool has_ellipsis() const
612  {
613  return find(ID_parameters).get_bool(ID_ellipsis);
614  }
615 
616  bool has_this() const
617  {
618  return get_this() != nullptr;
619  }
620 
621  const parametert *get_this() const
622  {
623  const parameterst &p=parameters();
624  if(!p.empty() && p.front().get_this())
625  return &p.front();
626  else
627  return nullptr;
628  }
629 
630  bool is_KnR() const
631  {
632  return get_bool(ID_C_KnR);
633  }
634 
636  {
637  add(ID_parameters).set(ID_ellipsis, true);
638  }
639 
641  {
642  add(ID_parameters).remove(ID_ellipsis);
643  }
644 
645  const typet &return_type() const
646  {
647  return find_type(ID_return_type);
648  }
649 
651  {
652  return add_type(ID_return_type);
653  }
654 
655  const parameterst &parameters() const
656  {
657  return (const parameterst &)find(ID_parameters).get_sub();
658  }
659 
661  {
662  return (parameterst &)add(ID_parameters).get_sub();
663  }
664 
665  bool get_inlined() const
666  {
667  return get_bool(ID_C_inlined);
668  }
669 
670  void set_inlined(bool value)
671  {
672  set(ID_C_inlined, value);
673  }
674 
675  const irep_idt &get_access() const
676  {
677  return get(ID_access);
678  }
679 
680  void set_access(const irep_idt &access)
681  {
682  return set(ID_access, access);
683  }
684 
685  bool get_is_constructor() const
686  {
687  return get_bool(ID_constructor);
688  }
689 
691  {
692  set(ID_constructor, true);
693  }
694 
696  std::vector<irep_idt> parameter_identifiers() const
697  {
698  std::vector<irep_idt> result;
699  const parameterst &p=parameters();
700  result.reserve(p.size());
701  for(parameterst::const_iterator it=p.begin();
702  it!=p.end(); it++)
703  result.push_back(it->get_identifier());
704  return result;
705  }
706 
707  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
708 
711  {
713  const parameterst &params = parameters();
714  parameter_indices.reserve(params.size());
715  std::size_t index = 0;
716  for(const auto &p : params)
717  {
718  const irep_idt &id = p.get_identifier();
719  if(!id.empty())
720  parameter_indices.insert({ id, index });
721  ++index;
722  }
723  return parameter_indices;
724  }
725 };
726 
730 template <>
731 inline bool can_cast_type<code_typet>(const typet &type)
732 {
733  return type.id() == ID_code;
734 }
735 
744 inline const code_typet &to_code_type(const typet &type)
745 {
747  code_typet::check(type);
748  return static_cast<const code_typet &>(type);
749 }
750 
753 {
755  code_typet::check(type);
756  return static_cast<code_typet &>(type);
757 }
758 
763 {
764 public:
765  array_typet(typet _subtype, exprt _size)
766  : type_with_subtypet(ID_array, std::move(_subtype))
767  {
768  add(ID_size, std::move(_size));
769  }
770 
772  typet index_type() const;
773 
778  {
779  return static_cast<typet &>(add(ID_C_index_type));
780  }
781 
785  const typet &element_type() const
786  {
787  return subtype();
788  }
789 
794  {
795  return subtype();
796  }
797 
798  // We will eventually enforce that the type of the size
799  // is the same as the index type.
800  const exprt &size() const
801  {
802  return static_cast<const exprt &>(find(ID_size));
803  }
804 
805  // We will eventually enforce that the type of the size
806  // is the same as the index type.
808  {
809  return static_cast<exprt &>(add(ID_size));
810  }
811 
812  bool is_complete() const
813  {
814  return size().is_not_nil();
815  }
816 
817  bool is_incomplete() const
818  {
819  return size().is_nil();
820  }
821 
822  static void check(
823  const typet &type,
825 };
826 
830 template <>
831 inline bool can_cast_type<array_typet>(const typet &type)
832 {
833  return type.id() == ID_array;
834 }
835 
844 inline const array_typet &to_array_type(const typet &type)
845 {
847  array_typet::check(type);
848  return static_cast<const array_typet &>(type);
849 }
850 
853 {
855  array_typet::check(type);
856  return static_cast<array_typet &>(type);
857 }
858 
864 class bitvector_typet : public typet
865 {
866 public:
867  explicit bitvector_typet(const irep_idt &_id) : typet(_id)
868  {
869  }
870 
871  bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
872  {
873  set_width(width);
874  }
875 
876  std::size_t get_width() const
877  {
878  return get_size_t(ID_width);
879  }
880 
881  void set_width(std::size_t width)
882  {
883  set_size_t(ID_width, width);
884  }
885 
886  static void check(
887  const typet &type,
889  {
890  DATA_CHECK(
891  vm, !type.get(ID_width).empty(), "bitvector type must have width");
892  }
893 };
894 
898 template <>
899 inline bool can_cast_type<bitvector_typet>(const typet &type)
900 {
901  return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
902  type.id() == ID_fixedbv || type.id() == ID_floatbv ||
903  type.id() == ID_verilog_signedbv ||
904  type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
905  type.id() == ID_pointer || type.id() == ID_c_bit_field ||
906  type.id() == ID_c_bool;
907 }
908 
912 class string_typet:public typet
913 {
914 public:
915  string_typet():typet(ID_string)
916  {
917  }
918 };
919 
923 template <>
924 inline bool can_cast_type<string_typet>(const typet &type)
925 {
926  return type.id() == ID_string;
927 }
928 
937 inline const string_typet &to_string_type(const typet &type)
938 {
940  return static_cast<const string_typet &>(type);
941 }
942 
945 {
947  return static_cast<string_typet &>(type);
948 }
949 
951 class range_typet:public typet
952 {
953 public:
954  range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
955  {
956  set_from(_from);
957  set_to(_to);
958  }
959 
960  mp_integer get_from() const;
961  mp_integer get_to() const;
962 
963  void set_from(const mp_integer &_from);
964  void set_to(const mp_integer &to);
965 };
966 
970 template <>
971 inline bool can_cast_type<range_typet>(const typet &type)
972 {
973  return type.id() == ID_range;
974 }
975 
984 inline const range_typet &to_range_type(const typet &type)
985 {
987  return static_cast<const range_typet &>(type);
988 }
989 
992 {
994  return static_cast<range_typet &>(type);
995 }
996 
1008 {
1009 public:
1011 
1013  typet index_type() const;
1014 
1019  {
1020  return static_cast<typet &>(add(ID_C_index_type));
1021  }
1022 
1026  const typet &element_type() const
1027  {
1028  return subtype();
1029  }
1030 
1035  {
1036  return subtype();
1037  }
1038 
1039  const constant_exprt &size() const;
1040  constant_exprt &size();
1041 };
1042 
1046 template <>
1047 inline bool can_cast_type<vector_typet>(const typet &type)
1048 {
1049  return type.id() == ID_vector;
1050 }
1051 
1060 inline const vector_typet &to_vector_type(const typet &type)
1061 {
1064  return static_cast<const vector_typet &>(type);
1065 }
1066 
1069 {
1072  return static_cast<vector_typet &>(type);
1073 }
1074 
1077 {
1078 public:
1079  explicit complex_typet(typet _subtype)
1080  : type_with_subtypet(ID_complex, std::move(_subtype))
1081  {
1082  }
1083 };
1084 
1088 template <>
1089 inline bool can_cast_type<complex_typet>(const typet &type)
1090 {
1091  return type.id() == ID_complex;
1092 }
1093 
1102 inline const complex_typet &to_complex_type(const typet &type)
1103 {
1106  return static_cast<const complex_typet &>(type);
1107 }
1108 
1111 {
1114  return static_cast<complex_typet &>(type);
1115 }
1116 
1118  const typet &type,
1119  const namespacet &ns);
1120 
1121 #endif // CPROVER_UTIL_STD_TYPES_H
Arrays with given size.
Definition: std_types.h:763
exprt & size()
Definition: std_types.h:807
typet & element_type()
The type of the elements of the array.
Definition: std_types.h:793
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.cpp:19
array_typet(typet _subtype, exprt _size)
Definition: std_types.h:765
bool is_incomplete() const
Definition: std_types.h:817
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:33
typet & index_type_nonconst()
The type of the index expressions into any instance of this type.
Definition: std_types.h:777
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:785
bool is_complete() const
Definition: std_types.h:812
const exprt & size() const
Definition: std_types.h:800
Base class of fixed-width bit-vector types.
Definition: std_types.h:865
void set_width(std::size_t width)
Definition: std_types.h:881
std::size_t get_width() const
Definition: std_types.h:876
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:886
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:871
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:867
The Boolean type.
Definition: std_types.h:36
bool_typet()
Definition: std_types.h:38
Class type.
Definition: std_types.h:325
componentst methodst
Definition: std_types.h:333
componentst static_memberst
Definition: std_types.h:346
const methodst & methods() const
Definition: std_types.h:335
methodst & methods()
Definition: std_types.h:340
bool is_abstract() const
Definition: std_types.h:358
componentt methodt
Definition: std_types.h:332
static_memberst & static_members()
Definition: std_types.h:353
componentt static_membert
Definition: std_types.h:345
const static_memberst & static_members() const
Definition: std_types.h:348
const exprt & default_value() const
Definition: std_types.h:562
exprt & default_value()
Definition: std_types.h:572
parametert(const typet &type)
Definition: std_types.h:558
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
bool get_this() const
Definition: std_types.h:600
bool has_default_value() const
Definition: std_types.h:567
const irep_idt & get_base_name() const
Definition: std_types.h:595
const irep_idt & get_identifier() const
Definition: std_types.h:590
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:580
Base type of functions.
Definition: std_types.h:539
bool is_KnR() const
Definition: std_types.h:630
code_typet(parameterst _parameters, typet _return_type)
Constructs a new code type, i.e., function type.
Definition: std_types.h:547
std::vector< parametert > parameterst
Definition: std_types.h:541
void set_is_constructor()
Definition: std_types.h:690
const typet & return_type() const
Definition: std_types.h:645
const irep_idt & get_access() const
Definition: std_types.h:675
void set_inlined(bool value)
Definition: std_types.h:670
bool has_this() const
Definition: std_types.h:616
bool get_inlined() const
Definition: std_types.h:665
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition: std_types.h:696
void set_access(const irep_idt &access)
Definition: std_types.h:680
parameterst & parameters()
Definition: std_types.h:660
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition: std_types.h:707
const parametert * get_this() const
Definition: std_types.h:621
bool get_is_constructor() const
Definition: std_types.h:685
void remove_ellipsis()
Definition: std_types.h:640
typet & return_type()
Definition: std_types.h:650
bool has_ellipsis() const
Definition: std_types.h:611
void make_ellipsis()
Definition: std_types.h:635
const parameterst & parameters() const
Definition: std_types.h:655
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition: std_types.h:710
Complex numbers made of pair of given subtype.
Definition: std_types.h:1077
complex_typet(typet _subtype)
Definition: std_types.h:1079
A constant literal expression.
Definition: std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
bool empty() const
Definition: dstring.h:90
The empty type.
Definition: std_types.h:51
An enumeration type, i.e., a type with elements (not to be confused with C enums)
Definition: std_types.h:490
const irept::subt & elements() const
Definition: std_types.h:496
irept::subt & elements()
Definition: std_types.h:501
Base class for all expressions.
Definition: expr.h:56
exprt & add_expr(const irep_idt &name)
Definition: expr.h:282
typet & type()
Return the type of the expression.
Definition: expr.h:84
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:287
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:456
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:67
const irept & find(const irep_idt &name) const
Definition: irep.cpp:105
tree_implementationt baset
Definition: irep.h:374
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void remove(const irep_idt &name)
Definition: irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:86
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
irept & add(const irep_idt &name)
Definition: irep.cpp:115
bool is_nil() const
Definition: irep.h:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
A type for subranges of integers.
Definition: std_types.h:952
void set_to(const mp_integer &to)
Definition: std_types.cpp:161
void set_from(const mp_integer &_from)
Definition: std_types.cpp:156
mp_integer get_to() const
Definition: std_types.cpp:171
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:954
mp_integer get_from() const
Definition: std_types.cpp:166
Base class for tree-like data structures with sharing.
Definition: irep.h:157
String type.
Definition: std_types.h:913
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:451
struct_tag_typet & type()
Definition: std_types.cpp:83
Structure type, corresponds to C style structs.
Definition: std_types.h:231
basest & bases()
Get the collection of base classes/structs.
Definition: std_types.h:268
struct_typet(componentst _components)
Definition: std_types.h:237
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
Definition: std_types.h:285
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:245
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
Definition: std_types.cpp:117
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:98
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:103
std::vector< baset > basest
Definition: std_types.h:259
const irep_idt & get_name() const
Definition: std_types.h:79
const irep_idt & get_base_name() const
Definition: std_types.h:89
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:114
void set_anonymous(bool anonymous)
Definition: std_types.h:124
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:94
const irep_idt & get_pretty_name() const
Definition: std_types.h:109
void set_is_padding(bool is_padding)
Definition: std_types.h:134
const irep_idt & get_access() const
Definition: std_types.h:99
void set_access(const irep_idt &access)
Definition: std_types.h:104
void set_name(const irep_idt &name)
Definition: std_types.h:84
componentt(const irep_idt &_name, typet _type)
Definition: std_types.h:73
Base type for structs and unions.
Definition: std_types.h:62
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:76
void set_tag(const irep_idt &tag)
Definition: std_types.h:169
irep_idt get_tag() const
Definition: std_types.h:168
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:172
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition: std_types.h:179
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:64
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:63
struct_union_typet(const irep_idt &_id, componentst _components)
Definition: std_types.h:142
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
const componentst & components() const
Definition: std_types.h:147
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:191
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:46
std::vector< componentt > componentst
Definition: std_types.h:140
componentst & components()
Definition: std_types.h:152
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
tag_typet(const irep_idt &_id, const irep_idt &identifier)
Definition: std_types.h:398
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:405
const irep_idt & get_identifier() const
Definition: std_types.h:410
Type with a single subtype.
Definition: type.h:165
const typet & subtype() const
Definition: type.h:172
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:184
The type of an expression, extends irept.
Definition: type.h:29
typet & add_type(const irep_idt &name)
Definition: type.h:100
const typet & find_type(const irep_idt &name) const
Definition: type.h:105
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:119
The vector type.
Definition: std_types.h:1008
vector_typet(typet index_type, typet element_type, constant_exprt size)
Definition: std_types.cpp:247
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
Definition: std_types.h:1018
const constant_exprt & size() const
Definition: std_types.cpp:269
typet & element_type()
The type of the elements of the vector.
Definition: std_types.h:1034
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1026
typet index_type() const
The type of any index expression into an instance of this type.
Definition: std_types.cpp:257
Templated functions to cast to specific exprt-derived classes.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:18
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1060
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition: std_types.h:368
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
Definition: std_types.cpp:185
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:984
bool can_cast_type< bool_typet >(const typet &base)
Definition: std_types.h:44
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:381
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
Definition: std_types.h:1089
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition: std_types.h:831
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition: std_types.h:1047
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:461
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:844
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition: std_types.h:937
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:731
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1102
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition: std_types.h:971
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_typet.
Definition: std_types.h:420
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
bool can_cast_type< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
Definition: std_types.h:511
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:899
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:524
bool can_cast_type< struct_union_typet >(const typet &type)
Check whether a reference to a typet is a struct_union_typet.
Definition: std_types.h:201
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
Definition: std_types.h:924
bool can_cast_type< struct_typet >(const typet &type)
Check whether a reference to a typet is a struct_typet.
Definition: std_types.h:295
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet