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"
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
777 const typet &element_type() const
778 {
779 return subtype();
780 }
781
786 {
787 return subtype();
788 }
789
790 const exprt &size() const
791 {
792 return static_cast<const exprt &>(find(ID_size));
793 }
794
796 {
797 return static_cast<exprt &>(add(ID_size));
798 }
799
800 bool is_complete() const
801 {
802 return size().is_not_nil();
803 }
804
805 bool is_incomplete() const
806 {
807 return size().is_nil();
808 }
809
810 static void check(
811 const typet &type,
813};
814
818template <>
819inline bool can_cast_type<array_typet>(const typet &type)
820{
821 return type.id() == ID_array;
822}
823
832inline const array_typet &to_array_type(const typet &type)
833{
835 array_typet::check(type);
836 return static_cast<const array_typet &>(type);
837}
838
841{
843 array_typet::check(type);
844 return static_cast<array_typet &>(type);
845}
846
852class bitvector_typet : public typet
853{
854public:
855 explicit bitvector_typet(const irep_idt &_id) : typet(_id)
856 {
857 }
858
859 bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
860 {
861 set_width(width);
862 }
863
864 std::size_t get_width() const
865 {
866 return get_size_t(ID_width);
867 }
868
869 void set_width(std::size_t width)
870 {
871 set_size_t(ID_width, width);
872 }
873
874 static void check(
875 const typet &type,
877 {
879 vm, !type.get(ID_width).empty(), "bitvector type must have width");
880 }
881};
882
886template <>
887inline bool can_cast_type<bitvector_typet>(const typet &type)
888{
889 return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
890 type.id() == ID_fixedbv || type.id() == ID_floatbv ||
891 type.id() == ID_verilog_signedbv ||
892 type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
893 type.id() == ID_pointer || type.id() == ID_c_bit_field ||
894 type.id() == ID_c_bool;
895}
896
900class string_typet:public typet
901{
902public:
903 string_typet():typet(ID_string)
904 {
905 }
906};
907
911template <>
912inline bool can_cast_type<string_typet>(const typet &type)
913{
914 return type.id() == ID_string;
915}
916
925inline const string_typet &to_string_type(const typet &type)
926{
928 return static_cast<const string_typet &>(type);
929}
930
933{
935 return static_cast<string_typet &>(type);
936}
937
939class range_typet:public typet
940{
941public:
942 range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
943 {
944 set_from(_from);
945 set_to(_to);
946 }
947
948 mp_integer get_from() const;
949 mp_integer get_to() const;
950
951 void set_from(const mp_integer &_from);
952 void set_to(const mp_integer &to);
953};
954
958template <>
959inline bool can_cast_type<range_typet>(const typet &type)
960{
961 return type.id() == ID_range;
962}
963
972inline const range_typet &to_range_type(const typet &type)
973{
975 return static_cast<const range_typet &>(type);
976}
977
980{
982 return static_cast<range_typet &>(type);
983}
984
996{
997public:
998 vector_typet(const typet &_subtype, const constant_exprt &_size);
999
1001 typet index_type() const;
1002
1006 const typet &element_type() const
1007 {
1008 return subtype();
1009 }
1010
1015 {
1016 return subtype();
1017 }
1018
1019 const constant_exprt &size() const;
1021};
1022
1026template <>
1027inline bool can_cast_type<vector_typet>(const typet &type)
1028{
1029 return type.id() == ID_vector;
1030}
1031
1040inline const vector_typet &to_vector_type(const typet &type)
1041{
1044 return static_cast<const vector_typet &>(type);
1045}
1046
1049{
1052 return static_cast<vector_typet &>(type);
1053}
1054
1057{
1058public:
1059 explicit complex_typet(typet _subtype)
1060 : type_with_subtypet(ID_complex, std::move(_subtype))
1061 {
1062 }
1063};
1064
1068template <>
1069inline bool can_cast_type<complex_typet>(const typet &type)
1070{
1071 return type.id() == ID_complex;
1072}
1073
1082inline const complex_typet &to_complex_type(const typet &type)
1083{
1086 return static_cast<const complex_typet &>(type);
1087}
1088
1091{
1094 return static_cast<complex_typet &>(type);
1095}
1096
1098 const typet &type,
1099 const namespacet &ns);
1100
1101#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:805
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:795
bool is_complete() const
Definition std_types.h:800
const exprt & size() const
Definition std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
typet & element_type()
The type of the elements of the array.
Definition std_types.h:785
Base class of fixed-width bit-vector types.
Definition std_types.h:853
void set_width(std::size_t width)
Definition std_types.h:869
std::size_t get_width() const
Definition std_types.h:864
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition std_types.h:874
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition std_types.h:859
bitvector_typet(const irep_idt &_id)
Definition std_types.h:855
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:1057
complex_typet(typet _subtype)
Definition std_types.h:1059
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
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:54
exprt & add_expr(const irep_idt &name)
Definition expr.h:301
typet & type()
Return the type of the expression.
Definition expr.h:82
const exprt & find_expr(const irep_idt &name) const
Definition expr.h:306
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void remove(const irep_idt &name)
Definition irep.cpp:96
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:87
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:116
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:940
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:942
mp_integer get_from() const
String type.
Definition std_types.h:901
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:77
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:92
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition std_types.cpp:97
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:70
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:57
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:40
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:149
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition type.h:168
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
typet & add_type(const irep_idt &name)
Definition type.h:84
const typet & find_type(const irep_idt &name) const
Definition type.h:89
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:103
The vector type.
Definition std_types.h:996
const constant_exprt & size() const
typet & element_type()
The type of the elements of the vector.
Definition std_types.h:1014
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:1006
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:12
#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:972
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:1069
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
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:819
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition std_types.h:1027
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition std_types.h:925
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:1082
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition std_types.h:959
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
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:887
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:912
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