cprover
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:
38 bool_typet():typet(ID_bool)
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:
53 empty_typet():typet(ID_empty)
54 {
55 }
56};
57
62{
63public:
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
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
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:
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
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
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
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
449{
450public:
451 explicit struct_tag_typet(const irep_idt &identifier):
452 tag_typet(ID_struct_tag, identifier)
453 {
454 }
455};
456
460template <>
462{
463 return type.id() == ID_struct_tag;
464}
465
474inline 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{
491public:
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
510template <>
512{
513 return type.id() == ID_enumeration;
514}
515
525{
527 return static_cast<const enumeration_typet &>(type);
528}
529
532{
534 return static_cast<enumeration_typet &>(type);
535}
536
538class code_typet:public typet
539{
540public:
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
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
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
730template <>
731inline bool can_cast_type<code_typet>(const typet &type)
732{
733 return type.id() == ID_code;
734}
735
744inline 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{
764public:
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
783 const typet &element_type() const
784 {
785 return subtype();
786 }
787
790 {
791 return subtype();
792 }
793
794 // We will eventually enforce that the type of the size
795 // is the same as the index type.
796 const exprt &size() const
797 {
798 return static_cast<const exprt &>(find(ID_size));
799 }
800
801 // We will eventually enforce that the type of the size
802 // is the same as the index type.
804 {
805 return static_cast<exprt &>(add(ID_size));
806 }
807
808 bool is_complete() const
809 {
810 return size().is_not_nil();
811 }
812
813 bool is_incomplete() const
814 {
815 return size().is_nil();
816 }
817
818 static void check(
819 const typet &type,
821
822protected:
823 // Use element_type() instead
825};
826
830template <>
831inline bool can_cast_type<array_typet>(const typet &type)
832{
833 return type.id() == ID_array;
834}
835
844inline 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
864class bitvector_typet : public typet
865{
866public:
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 {
891 vm, !type.get(ID_width).empty(), "bitvector type must have width");
892 }
893};
894
898template <>
899inline 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
912class string_typet:public typet
913{
914public:
915 string_typet():typet(ID_string)
916 {
917 }
918};
919
923template <>
924inline bool can_cast_type<string_typet>(const typet &type)
925{
926 return type.id() == ID_string;
927}
928
937inline 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
951class range_typet:public typet
952{
953public:
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
970template <>
971inline bool can_cast_type<range_typet>(const typet &type)
972{
973 return type.id() == ID_range;
974}
975
984inline 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{
1009public:
1011
1013 typet index_type() const;
1014
1019 {
1020 return static_cast<typet &>(add(ID_C_index_type));
1021 }
1022
1024 const typet &element_type() const
1025 {
1026 return subtype();
1027 }
1028
1031 {
1032 return subtype();
1033 }
1034
1035 const constant_exprt &size() const;
1037
1038protected:
1039 // Use element_type() instead
1041};
1042
1046template <>
1047inline bool can_cast_type<vector_typet>(const typet &type)
1048{
1049 return type.id() == ID_vector;
1050}
1051
1060inline 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{
1078public:
1079 explicit complex_typet(typet _subtype)
1080 : type_with_subtypet(ID_complex, std::move(_subtype))
1081 {
1082 }
1083};
1084
1088template <>
1089inline bool can_cast_type<complex_typet>(const typet &type)
1090{
1091 return type.id() == ID_complex;
1092}
1093
1102inline 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
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:813
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:33
exprt & size()
Definition std_types.h:803
bool is_complete() const
Definition std_types.h:808
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
const typet & subtype() const
Definition type.h:154
typet & index_type_nonconst()
The type of the index expressions into any instance of this type.
Definition std_types.h:777
typet & element_type()
The type of the elements of the array.
Definition std_types.h:789
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
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:558
const irep_idt & get_base_name() const
Definition std_types.h:595
const exprt & default_value() const
Definition std_types.h:562
void set_base_name(const irep_idt &name)
Definition std_types.h:585
const irep_idt & get_identifier() const
Definition std_types.h:590
bool get_this() const
Definition std_types.h:600
bool has_default_value() const
Definition std_types.h:567
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:542
typet & return_type()
Definition std_types.h:650
const irep_idt & get_access() const
Definition std_types.h:675
void set_is_constructor()
Definition std_types.h:690
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
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
parameterst & parameters()
Definition std_types.h:660
void set_access(const irep_idt &access)
Definition std_types.h:680
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition std_types.h:696
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition std_types.h:707
bool get_is_constructor() const
Definition std_types.h:685
void remove_ellipsis()
Definition std_types.h:640
bool has_ellipsis() const
Definition std_types.h:611
const parametert * get_this() const
Definition std_types.h:621
void make_ellipsis()
Definition std_types.h:635
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:294
typet & type()
Return the type of the expression.
Definition expr.h:84
const exprt & find_expr(const irep_idt &name) const
Definition expr.h:299
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:101
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
subt & get_sub()
Definition irep.h:456
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
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)
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:954
mp_integer get_from() const
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
Base class or struct that a class or struct inherits from.
Definition std_types.h:252
struct_tag_typet & type()
Definition std_types.cpp:83
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
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:98
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
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: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
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: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
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:46
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:147
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:166
const typet & subtype() const
Definition type.h:154
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:82
const typet & find_type(const irep_idt &name) const
Definition type.h:87
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:101
The vector type.
Definition std_types.h:1008
vector_typet(typet index_type, typet element_type, constant_exprt size)
const constant_exprt & size() const
typet & element_type()
The type of the elements of the vector.
Definition std_types.h:1030
const typet & subtype() const
Definition type.h:154
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
Definition std_types.h:1018
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:1024
Templated functions to cast to specific exprt-derived classes.
STL namespace.
nonstd::optional< T > optionalt
Definition optional.h:35
BigInt mp_integer
Definition smt_terms.h:18
#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:984
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:1089
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
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
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 string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition std_types.h:937
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 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:524
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< 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
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
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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: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
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 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