CBMC
Loading...
Searching...
No Matches
std_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pre-defined types
4
5Author: 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
24class constant_exprt;
25class namespacet;
26
29inline bool is_constant(const typet &type)
30{
31 return type.get_bool(ID_C_constant);
32}
33
35class bool_typet:public typet
36{
37public:
39 {
40 }
41};
42
43template <>
44inline bool can_cast_type<bool_typet>(const typet &base)
45{
46 return base.id() == ID_bool;
47}
48
50class empty_typet:public typet
51{
52public:
56};
57
62{
63public:
65 {
66 }
67
68 class componentt:public exprt
69 {
70 public:
71 componentt() = default;
72
74 {
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_C_base_name);
92 }
93
94 void set_base_name(const irep_idt &base_name)
95 {
96 return set(ID_C_base_name, base_name);
97 }
98
99 const irep_idt &get_access() const
100 {
101 return get(ID_access);
102 }
103
105 {
106 return set(ID_access, access);
107 }
108
110 {
111 return get(ID_C_pretty_name);
112 }
113
114 void set_pretty_name(const irep_idt &name)
115 {
116 return set(ID_C_pretty_name, name);
117 }
118
119 bool get_anonymous() const
120 {
121 return get_bool(ID_anonymous);
122 }
123
125 {
126 return set(ID_anonymous, anonymous);
127 }
128
129 bool get_is_padding() const
130 {
132 }
133
135 {
137 }
138 };
139
140 typedef std::vector<componentt> componentst;
141
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
200template <>
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
227class struct_tag_typet;
228
231{
232public:
236
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 std::optional<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
294template <>
295inline bool can_cast_type<struct_typet>(const typet &type)
296{
297 return type.id() == ID_struct;
298}
299
308inline 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{
326public:
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
357
358 bool is_abstract() const
359 {
360 return get_bool(ID_abstract);
361 }
362};
363
367template <>
368inline 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
381inline 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
395class tag_typet:public typet
396{
397public:
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
411 {
412 return get(ID_identifier);
413 }
414};
415
419template <>
420inline 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
434inline 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
451{
452protected:
453 struct_or_union_tag_typet(const irep_idt &id, const irep_idt &identifier)
454 : tag_typet(id, identifier)
455 {
457 }
458};
459
463template <>
465{
466 return type.id() == ID_struct_tag || type.id() == ID_union_tag;
467}
468
477inline const struct_or_union_tag_typet &
479{
481 return static_cast<const struct_or_union_tag_typet &>(type);
482}
483
490
493{
494public:
495 explicit struct_tag_typet(const irep_idt &identifier)
497 {
498 }
499};
500
504template <>
506{
507 return type.id() == ID_struct_tag;
508}
509
518inline const struct_tag_typet &to_struct_tag_type(const typet &type)
519{
521 return static_cast<const struct_tag_typet &>(type);
522}
523
526{
528 return static_cast<struct_tag_typet &>(type);
529}
530
534{
535public:
539
540 const irept::subt &elements() const
541 {
542 return find(ID_elements).get_sub();
543 }
544
546 {
547 return add(ID_elements).get_sub();
548 }
549};
550
554template <>
556{
557 return type.id() == ID_enumeration;
558}
559
569{
571 return static_cast<const enumeration_typet &>(type);
572}
573
576{
578 return static_cast<enumeration_typet &>(type);
579}
580
582class code_typet:public typet
583{
584public:
585 class parametert;
586 typedef std::vector<parametert> parameterst;
587
596
597 // used to be argumentt -- now uses standard terminology
598
599 class parametert:public exprt
600 {
601 public:
603 {
604 }
605
606 const exprt &default_value() const
607 {
609 }
610
611 bool has_default_value() const
612 {
613 return default_value().is_not_nil();
614 }
615
617 {
619 }
620
621 // The following for methods will go away;
622 // these should not be part of the signature of a function,
623 // but rather part of the body.
624 void set_identifier(const irep_idt &identifier)
625 {
626 set(ID_C_identifier, identifier);
627 }
628
629 void set_base_name(const irep_idt &name)
630 {
631 set(ID_C_base_name, name);
632 }
633
635 {
636 return get(ID_C_identifier);
637 }
638
639 const irep_idt &get_base_name() const
640 {
641 return get(ID_C_base_name);
642 }
643
644 bool get_this() const
645 {
646 return get_bool(ID_C_this);
647 }
648
649 void set_this()
650 {
651 set(ID_C_this, true);
652 }
653 };
654
655 bool has_ellipsis() const
656 {
657 return find(ID_parameters).get_bool(ID_ellipsis);
658 }
659
660 bool has_this() const
661 {
662 return get_this() != nullptr;
663 }
664
665 const parametert *get_this() const
666 {
667 const parameterst &p=parameters();
668 if(!p.empty() && p.front().get_this())
669 return &p.front();
670 else
671 return nullptr;
672 }
673
674 bool is_KnR() const
675 {
676 return get_bool(ID_C_KnR);
677 }
678
680 {
682 }
683
688
689 const typet &return_type() const
690 {
692 }
693
695 {
696 return add_type(ID_return_type);
697 }
698
699 const parameterst &parameters() const
700 {
701 return (const parameterst &)find(ID_parameters).get_sub();
702 }
703
705 {
707 }
708
709 bool get_inlined() const
710 {
711 return get_bool(ID_C_inlined);
712 }
713
714 void set_inlined(bool value)
715 {
716 set(ID_C_inlined, value);
717 }
718
719 const irep_idt &get_access() const
720 {
721 return get(ID_access);
722 }
723
725 {
726 return set(ID_access, access);
727 }
728
730 {
731 return get_bool(ID_constructor);
732 }
733
735 {
736 set(ID_constructor, true);
737 }
738
740 std::vector<irep_idt> parameter_identifiers() const
741 {
742 std::vector<irep_idt> result;
743 const parameterst &p=parameters();
744 result.reserve(p.size());
745 for(parameterst::const_iterator it=p.begin();
746 it!=p.end(); it++)
747 result.push_back(it->get_identifier());
748 return result;
749 }
750
751 typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
752
755 {
757 const parameterst &params = parameters();
758 parameter_indices.reserve(params.size());
759 std::size_t index = 0;
760 for(const auto &p : params)
761 {
762 const irep_idt &id = p.get_identifier();
763 if(!id.empty())
764 parameter_indices.insert({ id, index });
765 ++index;
766 }
767 return parameter_indices;
768 }
769};
770
774template <>
775inline bool can_cast_type<code_typet>(const typet &type)
776{
777 return type.id() == ID_code;
778}
779
788inline const code_typet &to_code_type(const typet &type)
789{
791 code_typet::check(type);
792 return static_cast<const code_typet &>(type);
793}
794
797{
799 code_typet::check(type);
800 return static_cast<code_typet &>(type);
801}
802
807{
808public:
811 {
812 add(ID_size, std::move(_size));
813 }
814
816 typet index_type() const;
817
822 {
823 return static_cast<typet &>(add(ID_C_index_type));
824 }
825
827 const typet &element_type() const
828 {
829 return subtype();
830 }
831
834 {
835 return subtype();
836 }
837
838 // We will eventually enforce that the type of the size
839 // is the same as the index type.
840 const exprt &size() const
841 {
842 return static_cast<const exprt &>(find(ID_size));
843 }
844
845 // We will eventually enforce that the type of the size
846 // is the same as the index type.
848 {
849 return static_cast<exprt &>(add(ID_size));
850 }
851
852 bool is_complete() const
853 {
854 return size().is_not_nil();
855 }
856
857 bool is_incomplete() const
858 {
859 return size().is_nil();
860 }
861
862 static void check(
863 const typet &type,
865
866protected:
867 // Use element_type() instead
869};
870
874template <>
875inline bool can_cast_type<array_typet>(const typet &type)
876{
877 return type.id() == ID_array;
878}
879
888inline const array_typet &to_array_type(const typet &type)
889{
891 array_typet::check(type);
892 return static_cast<const array_typet &>(type);
893}
894
897{
899 array_typet::check(type);
900 return static_cast<array_typet &>(type);
901}
902
908class bitvector_typet : public typet
909{
910public:
912 {
913 }
914
915 bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
916 {
918 }
919
921 {
922 width(_width);
923 }
924
925 std::size_t get_width() const
926 {
927 return get_size_t(ID_width);
928 }
929
930 std::size_t width() const;
931
932 void set_width(std::size_t width)
933 {
935 }
936
937 void width(const mp_integer &);
938
939 static void check(
940 const typet &type,
942 {
944 vm, !type.get(ID_width).empty(), "bitvector type must have width");
945 }
946};
947
951template <>
952inline bool can_cast_type<bitvector_typet>(const typet &type)
953{
954 return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
955 type.id() == ID_fixedbv || type.id() == ID_floatbv ||
956 type.id() == ID_verilog_signedbv ||
957 type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
958 type.id() == ID_pointer || type.id() == ID_c_bit_field ||
959 type.id() == ID_c_bool;
960}
961
965class string_typet:public typet
966{
967public:
971};
972
976template <>
977inline bool can_cast_type<string_typet>(const typet &type)
978{
979 return type.id() == ID_string;
980}
981
990inline const string_typet &to_string_type(const typet &type)
991{
993 return static_cast<const string_typet &>(type);
994}
995
998{
1000 return static_cast<string_typet &>(type);
1001}
1002
1004class range_typet:public typet
1005{
1006public:
1008 {
1009 set_from(_from);
1010 set_to(_to);
1011 }
1012
1013 mp_integer get_from() const;
1014 mp_integer get_to() const;
1015 bool includes(const mp_integer &) const;
1016 constant_exprt zero_expr() const;
1017 constant_exprt one_expr() const;
1018
1019 void set_from(const mp_integer &_from);
1020 void set_to(const mp_integer &to);
1021};
1022
1026template <>
1027inline bool can_cast_type<range_typet>(const typet &type)
1028{
1029 return type.id() == ID_range;
1030}
1031
1040inline const range_typet &to_range_type(const typet &type)
1041{
1043 return static_cast<const range_typet &>(type);
1044}
1045
1048{
1050 return static_cast<range_typet &>(type);
1051}
1052
1064{
1065public:
1067
1069 typet index_type() const;
1070
1075 {
1076 return static_cast<typet &>(add(ID_C_index_type));
1077 }
1078
1080 const typet &element_type() const
1081 {
1082 return subtype();
1083 }
1084
1087 {
1088 return subtype();
1089 }
1090
1091 const constant_exprt &size() const;
1093
1094protected:
1095 // Use element_type() instead
1097};
1098
1102template <>
1103inline bool can_cast_type<vector_typet>(const typet &type)
1104{
1105 return type.id() == ID_vector;
1106}
1107
1116inline const vector_typet &to_vector_type(const typet &type)
1117{
1120 return static_cast<const vector_typet &>(type);
1121}
1122
1125{
1128 return static_cast<vector_typet &>(type);
1129}
1130
1133{
1134public:
1137 {
1138 }
1139};
1140
1144template <>
1145inline bool can_cast_type<complex_typet>(const typet &type)
1146{
1147 return type.id() == ID_complex;
1148}
1149
1158inline const complex_typet &to_complex_type(const typet &type)
1159{
1162 return static_cast<const complex_typet &>(type);
1163}
1164
1167{
1170 return static_cast<complex_typet &>(type);
1171}
1172
1174 const typet &type,
1175 const namespacet &ns);
1176
1177#endif // CPROVER_UTIL_STD_TYPES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Arrays with given size.
Definition std_types.h:807
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition std_types.cpp:20
array_typet(typet _subtype, exprt _size)
Definition std_types.h:809
bool is_incomplete() const
Definition std_types.h:857
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
exprt & size()
Definition std_types.h:847
bool is_complete() const
Definition std_types.h:852
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
const typet & subtype() const
Definition type.h:187
typet & index_type_nonconst()
The type of the index expressions into any instance of this type.
Definition std_types.h:821
typet & element_type()
The type of the elements of the array.
Definition std_types.h:833
Base class of fixed-width bit-vector types.
Definition std_types.h:909
void set_width(std::size_t width)
Definition std_types.h:932
std::size_t get_width() const
Definition std_types.h:925
std::size_t width() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition std_types.h:939
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition std_types.h:915
bitvector_typet(const irep_idt &_id, mp_integer _width)
Definition std_types.h:920
bitvector_typet(const irep_idt &_id)
Definition std_types.h:911
The Boolean type.
Definition std_types.h:36
Class type.
Definition std_types.h:325
componentst methodst
Definition std_types.h:333
componentst static_memberst
Definition std_types.h:346
methodst & methods()
Definition std_types.h:340
static_memberst & static_members()
Definition std_types.h:353
bool is_abstract() const
Definition std_types.h:358
componentt methodt
Definition std_types.h:332
componentt static_membert
Definition std_types.h:345
const methodst & methods() const
Definition std_types.h:335
const static_memberst & static_members() const
Definition std_types.h:348
parametert(const typet &type)
Definition std_types.h:602
const irep_idt & get_base_name() const
Definition std_types.h:639
const exprt & default_value() const
Definition std_types.h:606
void set_base_name(const irep_idt &name)
Definition std_types.h:629
const irep_idt & get_identifier() const
Definition std_types.h:634
bool get_this() const
Definition std_types.h:644
bool has_default_value() const
Definition std_types.h:611
void set_identifier(const irep_idt &identifier)
Definition std_types.h:624
Base type of functions.
Definition std_types.h:583
bool is_KnR() const
Definition std_types.h:674
code_typet(parameterst _parameters, typet _return_type)
Constructs a new code type, i.e., function type.
Definition std_types.h:591
std::vector< parametert > parameterst
Definition std_types.h:586
typet & return_type()
Definition std_types.h:694
const irep_idt & get_access() const
Definition std_types.h:719
void set_is_constructor()
Definition std_types.h:734
void set_inlined(bool value)
Definition std_types.h:714
bool has_this() const
Definition std_types.h:660
bool get_inlined() const
Definition std_types.h:709
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
parameterst & parameters()
Definition std_types.h:704
void set_access(const irep_idt &access)
Definition std_types.h:724
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition std_types.h:740
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition std_types.h:751
bool get_is_constructor() const
Definition std_types.h:729
void remove_ellipsis()
Definition std_types.h:684
bool has_ellipsis() const
Definition std_types.h:655
const parametert * get_this() const
Definition std_types.h:665
void make_ellipsis()
Definition std_types.h:679
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition std_types.h:754
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
complex_typet(typet _subtype)
Definition std_types.h:1135
A constant literal expression.
Definition std_expr.h:3117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:534
const irept::subt & elements() const
Definition std_types.h:540
irept::subt & elements()
Definition std_types.h:545
Base class for all expressions.
Definition expr.h:56
exprt & add_expr(const irep_idt &name)
Definition expr.h:302
typet & type()
Return the type of the expression.
Definition expr.h:84
const exprt & find_expr(const irep_idt &name) const
Definition expr.h:307
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:82
subt & get_sub()
Definition irep.h:448
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
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:1005
void set_to(const mp_integer &to)
constant_exprt zero_expr() const
void set_from(const mp_integer &_from)
mp_integer get_to() const
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition std_types.h:1007
bool includes(const mp_integer &) const
constant_exprt one_expr() const
mp_integer get_from() const
String type.
Definition std_types.h:966
A struct or union tag type.
Definition std_types.h:451
struct_or_union_tag_typet(const irep_idt &id, const irep_idt &identifier)
Definition std_types.h:453
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
struct_tag_typet(const irep_idt &identifier)
Definition std_types.h:495
Base class or struct that a class or struct inherits from.
Definition std_types.h:252
struct_tag_typet & type()
Definition std_types.cpp:84
Structure type, corresponds to C style structs.
Definition std_types.h:231
const basest & bases() const
Get the collection of base classes/structs.
Definition std_types.h:262
std::optional< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
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
basest & bases()
Get the collection of base classes/structs.
Definition std_types.h:268
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...
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition std_types.cpp:99
std::vector< baset > basest
Definition std_types.h:259
const irep_idt & get_pretty_name() const
Definition std_types.h:109
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_access() const
Definition std_types.h:99
void set_is_padding(bool is_padding)
Definition std_types.h:134
const irep_idt & get_base_name() const
Definition std_types.h:89
void set_access(const irep_idt &access)
Definition std_types.h:104
const irep_idt & get_name() const
Definition std_types.h:79
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:77
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
const componentst & components() const
Definition std_types.h:147
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:64
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
void make_incomplete()
A struct/union may be incomplete.
Definition std_types.h:191
componentst & components()
Definition std_types.h:152
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:47
std::vector< componentt > componentst
Definition std_types.h:140
A tag-based type, i.e., typet with an identifier.
Definition std_types.h:396
const irep_idt & get_identifier() const
Definition std_types.h:410
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
Type with a single subtype.
Definition type.h:180
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:199
const typet & subtype() const
Definition type.h:187
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:115
const typet & find_type(const irep_idt &name) const
Definition type.h:120
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:134
The vector type.
Definition std_types.h:1064
const constant_exprt & size() const
typet & element_type()
The type of the elements of the vector.
Definition std_types.h:1086
const typet & subtype() const
Definition type.h:187
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
Definition std_types.h:1074
typet index_type() const
The type of any index expression into an instance of this type.
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1080
Templated functions to cast to specific exprt-derived classes.
STL namespace.
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition std_types.h:1040
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.
bool can_cast_type< bool_typet >(const typet &base)
Definition std_types.h:44
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
Definition std_types.h:1145
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:875
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition std_types.h:1103
bool can_cast_type< struct_or_union_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_or_union_tag_typet.
Definition std_types.h:464
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition std_types.h:990
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:505
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition std_types.h:568
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition std_types.h:775
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition std_types.h:1027
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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_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< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
Definition std_types.h:555
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:952
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:977
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 class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition std_types.h:381
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