cprover
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"
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 
44 class empty_typet:public typet
45 {
46 public:
47  empty_typet():typet(ID_empty)
48  {
49  }
50 };
51 
56 {
57 public:
58  explicit struct_union_typet(const irep_idt &_id):typet(_id)
59  {
60  }
61 
62  class componentt:public exprt
63  {
64  public:
65  componentt() = default;
66 
67  componentt(const irep_idt &_name, typet _type)
68  {
69  set_name(_name);
70  type().swap(_type);
71  }
72 
73  const irep_idt &get_name() const
74  {
75  return get(ID_name);
76  }
77 
78  void set_name(const irep_idt &name)
79  {
80  return set(ID_name, name);
81  }
82 
83  const irep_idt &get_base_name() const
84  {
85  return get(ID_base_name);
86  }
87 
88  void set_base_name(const irep_idt &base_name)
89  {
90  return set(ID_base_name, base_name);
91  }
92 
93  const irep_idt &get_access() const
94  {
95  return get(ID_access);
96  }
97 
98  void set_access(const irep_idt &access)
99  {
100  return set(ID_access, access);
101  }
102 
103  const irep_idt &get_pretty_name() const
104  {
105  return get(ID_pretty_name);
106  }
107 
108  void set_pretty_name(const irep_idt &name)
109  {
110  return set(ID_pretty_name, name);
111  }
112 
113  bool get_anonymous() const
114  {
115  return get_bool(ID_anonymous);
116  }
117 
118  void set_anonymous(bool anonymous)
119  {
120  return set(ID_anonymous, anonymous);
121  }
122 
123  bool get_is_padding() const
124  {
125  return get_bool(ID_C_is_padding);
126  }
127 
128  void set_is_padding(bool is_padding)
129  {
130  return set(ID_C_is_padding, is_padding);
131  }
132  };
133 
134  typedef std::vector<componentt> componentst;
135 
136  struct_union_typet(const irep_idt &_id, componentst _components) : typet(_id)
137  {
138  components() = std::move(_components);
139  }
140 
141  const componentst &components() const
142  {
143  return (const componentst &)(find(ID_components).get_sub());
144  }
145 
147  {
148  return (componentst &)(add(ID_components).get_sub());
149  }
150 
151  bool has_component(const irep_idt &component_name) const
152  {
153  return get_component(component_name).is_not_nil();
154  }
155 
156  const componentt &get_component(
157  const irep_idt &component_name) const;
158 
159  std::size_t component_number(const irep_idt &component_name) const;
160  const typet &component_type(const irep_idt &component_name) const;
161 
162  irep_idt get_tag() const { return get(ID_tag); }
163  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
164 
166  bool is_class() const
167  {
168  return id() == ID_struct && get_bool(ID_C_class);
169  }
170 
174  {
175  return is_class() ? ID_private : ID_public;
176  }
177 
179  bool is_incomplete() const
180  {
181  return get_bool(ID_incomplete);
182  }
183 
186  {
187  set(ID_incomplete, true);
188  }
189 };
190 
194 template <>
195 inline bool can_cast_type<struct_union_typet>(const typet &type)
196 {
197  return type.id() == ID_struct || type.id() == ID_union;
198 }
199 
209 {
211  return static_cast<const struct_union_typet &>(type);
212 }
213 
216 {
218  return static_cast<struct_union_typet &>(type);
219 }
220 
221 class struct_tag_typet;
222 
225 {
226 public:
228  {
229  }
230 
231  explicit struct_typet(componentst _components)
232  : struct_union_typet(ID_struct, std::move(_components))
233  {
234  }
235 
236  bool is_prefix_of(const struct_typet &other) const;
237 
239  bool is_class() const
240  {
241  return get_bool(ID_C_class);
242  }
243 
245  class baset : public exprt
246  {
247  public:
249  const struct_tag_typet &type() const;
250  explicit baset(struct_tag_typet base);
251  };
252 
253  typedef std::vector<baset> basest;
254 
256  const basest &bases() const
257  {
258  return (const basest &)find(ID_bases).get_sub();
259  }
260 
263  {
264  return (basest &)add(ID_bases).get_sub();
265  }
266 
269  void add_base(const struct_tag_typet &base);
270 
274  optionalt<baset> get_base(const irep_idt &id) const;
275 
279  bool has_base(const irep_idt &id) const
280  {
281  return get_base(id).has_value();
282  }
283 };
284 
288 template <>
289 inline bool can_cast_type<struct_typet>(const typet &type)
290 {
291  return type.id() == ID_struct;
292 }
293 
302 inline const struct_typet &to_struct_type(const typet &type)
303 {
305  return static_cast<const struct_typet &>(type);
306 }
307 
310 {
312  return static_cast<struct_typet &>(type);
313 }
314 
319 {
320 public:
322  {
323  set(ID_C_class, true);
324  }
325 
328 
329  const methodst &methods() const
330  {
331  return (const methodst &)(find(ID_methods).get_sub());
332  }
333 
335  {
336  return (methodst &)(add(ID_methods).get_sub());
337  }
338 
341 
343  {
344  return (const static_memberst &)(find(ID_static_members).get_sub());
345  }
346 
348  {
349  return (static_memberst &)(add(ID_static_members).get_sub());
350  }
351 
352  bool is_abstract() const
353  {
354  return get_bool(ID_abstract);
355  }
356 };
357 
361 template <>
362 inline bool can_cast_type<class_typet>(const typet &type)
363 {
364  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
365 }
366 
375 inline const class_typet &to_class_type(const typet &type)
376 {
378  return static_cast<const class_typet &>(type);
379 }
380 
383 {
385  return static_cast<class_typet &>(type);
386 }
387 
389 class tag_typet:public typet
390 {
391 public:
392  explicit tag_typet(
393  const irep_idt &_id,
394  const irep_idt &identifier):typet(_id)
395  {
396  set_identifier(identifier);
397  }
398 
399  void set_identifier(const irep_idt &identifier)
400  {
401  set(ID_identifier, identifier);
402  }
403 
404  const irep_idt &get_identifier() const
405  {
406  return get(ID_identifier);
407  }
408 };
409 
413 template <>
414 inline bool can_cast_type<tag_typet>(const typet &type)
415 {
416  return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
417  type.id() == ID_union_tag;
418 }
419 
428 inline const tag_typet &to_tag_type(const typet &type)
429 {
431  return static_cast<const tag_typet &>(type);
432 }
433 
436 {
438  return static_cast<tag_typet &>(type);
439 }
440 
443 {
444 public:
445  explicit struct_tag_typet(const irep_idt &identifier):
446  tag_typet(ID_struct_tag, identifier)
447  {
448  }
449 };
450 
454 template <>
455 inline bool can_cast_type<struct_tag_typet>(const typet &type)
456 {
457  return type.id() == ID_struct_tag;
458 }
459 
468 inline const struct_tag_typet &to_struct_tag_type(const typet &type)
469 {
471  return static_cast<const struct_tag_typet &>(type);
472 }
473 
476 {
478  return static_cast<struct_tag_typet &>(type);
479 }
480 
484 {
485 public:
486  enumeration_typet():typet(ID_enumeration)
487  {
488  }
489 
490  const irept::subt &elements() const
491  {
492  return find(ID_elements).get_sub();
493  }
494 
496  {
497  return add(ID_elements).get_sub();
498  }
499 };
500 
504 template <>
505 inline bool can_cast_type<enumeration_typet>(const typet &type)
506 {
507  return type.id() == ID_enumeration;
508 }
509 
518 inline const enumeration_typet &to_enumeration_type(const typet &type)
519 {
521  return static_cast<const enumeration_typet &>(type);
522 }
523 
526 {
528  return static_cast<enumeration_typet &>(type);
529 }
530 
532 class code_typet:public typet
533 {
534 public:
535  class parametert;
536  typedef std::vector<parametert> parameterst;
537 
541  code_typet(parameterst _parameters, typet _return_type) : typet(ID_code)
542  {
543  parameters().swap(_parameters);
544  return_type().swap(_return_type);
545  }
546 
547  // used to be argumentt -- now uses standard terminology
548 
549  class parametert:public exprt
550  {
551  public:
552  explicit parametert(const typet &type):exprt(ID_parameter, type)
553  {
554  }
555 
556  const exprt &default_value() const
557  {
558  return find_expr(ID_C_default_value);
559  }
560 
561  bool has_default_value() const
562  {
563  return default_value().is_not_nil();
564  }
565 
567  {
568  return add_expr(ID_C_default_value);
569  }
570 
571  // The following for methods will go away;
572  // these should not be part of the signature of a function,
573  // but rather part of the body.
574  void set_identifier(const irep_idt &identifier)
575  {
576  set(ID_C_identifier, identifier);
577  }
578 
579  void set_base_name(const irep_idt &name)
580  {
581  set(ID_C_base_name, name);
582  }
583 
584  const irep_idt &get_identifier() const
585  {
586  return get(ID_C_identifier);
587  }
588 
589  const irep_idt &get_base_name() const
590  {
591  return get(ID_C_base_name);
592  }
593 
594  bool get_this() const
595  {
596  return get_bool(ID_C_this);
597  }
598 
599  void set_this()
600  {
601  set(ID_C_this, true);
602  }
603  };
604 
605  bool has_ellipsis() const
606  {
607  return find(ID_parameters).get_bool(ID_ellipsis);
608  }
609 
610  bool has_this() const
611  {
612  return get_this() != nullptr;
613  }
614 
615  const parametert *get_this() const
616  {
617  const parameterst &p=parameters();
618  if(!p.empty() && p.front().get_this())
619  return &p.front();
620  else
621  return nullptr;
622  }
623 
624  bool is_KnR() const
625  {
626  return get_bool(ID_C_KnR);
627  }
628 
630  {
631  add(ID_parameters).set(ID_ellipsis, true);
632  }
633 
635  {
636  add(ID_parameters).remove(ID_ellipsis);
637  }
638 
639  const typet &return_type() const
640  {
641  return find_type(ID_return_type);
642  }
643 
645  {
646  return add_type(ID_return_type);
647  }
648 
649  const parameterst &parameters() const
650  {
651  return (const parameterst &)find(ID_parameters).get_sub();
652  }
653 
655  {
656  return (parameterst &)add(ID_parameters).get_sub();
657  }
658 
659  bool get_inlined() const
660  {
661  return get_bool(ID_C_inlined);
662  }
663 
664  void set_inlined(bool value)
665  {
666  set(ID_C_inlined, value);
667  }
668 
669  const irep_idt &get_access() const
670  {
671  return get(ID_access);
672  }
673 
674  void set_access(const irep_idt &access)
675  {
676  return set(ID_access, access);
677  }
678 
679  bool get_is_constructor() const
680  {
681  return get_bool(ID_constructor);
682  }
683 
685  {
686  set(ID_constructor, true);
687  }
688 
690  std::vector<irep_idt> parameter_identifiers() const
691  {
692  std::vector<irep_idt> result;
693  const parameterst &p=parameters();
694  result.reserve(p.size());
695  for(parameterst::const_iterator it=p.begin();
696  it!=p.end(); it++)
697  result.push_back(it->get_identifier());
698  return result;
699  }
700 
701  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
702 
705  {
707  const parameterst &params = parameters();
708  parameter_indices.reserve(params.size());
709  std::size_t index = 0;
710  for(const auto &p : params)
711  {
712  const irep_idt &id = p.get_identifier();
713  if(!id.empty())
714  parameter_indices.insert({ id, index });
715  ++index;
716  }
717  return parameter_indices;
718  }
719 };
720 
724 template <>
725 inline bool can_cast_type<code_typet>(const typet &type)
726 {
727  return type.id() == ID_code;
728 }
729 
738 inline const code_typet &to_code_type(const typet &type)
739 {
741  code_typet::check(type);
742  return static_cast<const code_typet &>(type);
743 }
744 
747 {
749  code_typet::check(type);
750  return static_cast<code_typet &>(type);
751 }
752 
757 {
758 public:
759  array_typet(typet _subtype, exprt _size)
760  : type_with_subtypet(ID_array, std::move(_subtype))
761  {
762  add(ID_size, std::move(_size));
763  }
764 
765  const exprt &size() const
766  {
767  return static_cast<const exprt &>(find(ID_size));
768  }
769 
771  {
772  return static_cast<exprt &>(add(ID_size));
773  }
774 
775  bool is_complete() const
776  {
777  return size().is_not_nil();
778  }
779 
780  bool is_incomplete() const
781  {
782  return size().is_nil();
783  }
784 
785  static void check(
786  const typet &type,
788 };
789 
793 template <>
794 inline bool can_cast_type<array_typet>(const typet &type)
795 {
796  return type.id() == ID_array;
797 }
798 
807 inline const array_typet &to_array_type(const typet &type)
808 {
810  return static_cast<const array_typet &>(type);
811 }
812 
815 {
817  return static_cast<array_typet &>(type);
818 }
819 
825 class bitvector_typet : public typet
826 {
827 public:
828  explicit bitvector_typet(const irep_idt &_id) : typet(_id)
829  {
830  }
831 
832  bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
833  {
834  set_width(width);
835  }
836 
837  std::size_t get_width() const
838  {
839  return get_size_t(ID_width);
840  }
841 
842  void set_width(std::size_t width)
843  {
844  set_size_t(ID_width, width);
845  }
846 
847  static void check(
848  const typet &type,
850  {
851  DATA_CHECK(
852  vm, !type.get(ID_width).empty(), "bitvector type must have width");
853  }
854 };
855 
859 template <>
860 inline bool can_cast_type<bitvector_typet>(const typet &type)
861 {
862  return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
863  type.id() == ID_fixedbv || type.id() == ID_floatbv ||
864  type.id() == ID_verilog_signedbv ||
865  type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
866  type.id() == ID_pointer || type.id() == ID_c_bit_field ||
867  type.id() == ID_c_bool;
868 }
869 
873 class string_typet:public typet
874 {
875 public:
876  string_typet():typet(ID_string)
877  {
878  }
879 };
880 
884 template <>
885 inline bool can_cast_type<string_typet>(const typet &type)
886 {
887  return type.id() == ID_string;
888 }
889 
898 inline const string_typet &to_string_type(const typet &type)
899 {
901  return static_cast<const string_typet &>(type);
902 }
903 
906 {
908  return static_cast<string_typet &>(type);
909 }
910 
912 class range_typet:public typet
913 {
914 public:
915  range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
916  {
917  set_from(_from);
918  set_to(_to);
919  }
920 
921  mp_integer get_from() const;
922  mp_integer get_to() const;
923 
924  void set_from(const mp_integer &_from);
925  void set_to(const mp_integer &to);
926 };
927 
931 template <>
932 inline bool can_cast_type<range_typet>(const typet &type)
933 {
934  return type.id() == ID_range;
935 }
936 
945 inline const range_typet &to_range_type(const typet &type)
946 {
948  return static_cast<const range_typet &>(type);
949 }
950 
953 {
955  return static_cast<range_typet &>(type);
956 }
957 
969 {
970 public:
971  vector_typet(const typet &_subtype, const constant_exprt &_size);
972 
973  const constant_exprt &size() const;
974  constant_exprt &size();
975 };
976 
980 template <>
981 inline bool can_cast_type<vector_typet>(const typet &type)
982 {
983  return type.id() == ID_vector;
984 }
985 
994 inline const vector_typet &to_vector_type(const typet &type)
995 {
997  return static_cast<const vector_typet &>(type);
998 }
999 
1002 {
1004  return static_cast<vector_typet &>(type);
1005 }
1006 
1009 {
1010 public:
1011  explicit complex_typet(typet _subtype)
1012  : type_with_subtypet(ID_complex, std::move(_subtype))
1013  {
1014  }
1015 };
1016 
1020 template <>
1021 inline bool can_cast_type<complex_typet>(const typet &type)
1022 {
1023  return type.id() == ID_complex;
1024 }
1025 
1034 inline const complex_typet &to_complex_type(const typet &type)
1035 {
1037  return static_cast<const complex_typet &>(type);
1038 }
1039 
1042 {
1044  return static_cast<complex_typet &>(type);
1045 }
1046 
1048  const typet &type,
1049  const namespacet &ns);
1050 
1051 #endif // CPROVER_UTIL_STD_TYPES_H
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
array_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.cpp:22
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:605
to_enumeration_type
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:518
struct_tag_typet::struct_tag_typet
struct_tag_typet(const irep_idt &identifier)
Definition: std_types.h:445
tag_typet::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:399
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
struct_typet::get_base
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
Definition: std_types.cpp:93
class_typet::methodst
componentst methodst
Definition: std_types.h:327
array_typet::is_incomplete
bool is_incomplete() const
Definition: std_types.h:780
exprt::find_expr
const exprt & find_expr(const irep_idt &name) const
Definition: expr.h:314
class_typet
Class type.
Definition: std_types.h:319
struct_union_typet::componentt::get_anonymous
bool get_anonymous() const
Definition: std_types.h:113
struct_union_typet::componentt::componentt
componentt(const irep_idt &_name, typet _type)
Definition: std_types.h:67
mp_arith.h
struct_union_typet::componentt::componentt
componentt()=default
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
code_typet::parametert::default_value
exprt & default_value()
Definition: std_types.h:566
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
struct_union_typet::componentt::set_access
void set_access(const irep_idt &access)
Definition: std_types.h:98
enumeration_typet
An enumeration type, i.e., a type with elements (not to be confused with C enums)
Definition: std_types.h:484
struct_union_typet::componentt::set_anonymous
void set_anonymous(bool anonymous)
Definition: std_types.h:118
class_typet::is_abstract
bool is_abstract() const
Definition: std_types.h:352
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
array_typet::is_complete
bool is_complete() const
Definition: std_types.h:775
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
tag_typet::tag_typet
tag_typet(const irep_idt &_id, const irep_idt &identifier)
Definition: std_types.h:392
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:375
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:574
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
class_typet::static_members
static_memberst & static_members()
Definition: std_types.h:347
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
struct_typet::has_base
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
Definition: std_types.h:279
empty_typet::empty_typet
empty_typet()
Definition: std_types.h:47
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
struct_typet::is_prefix_of
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:107
can_cast_type< complex_typet >
bool can_cast_type< complex_typet >(const typet &type)
Check whether a reference to a typet is a complex_typet.
Definition: std_types.h:1021
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
struct_union_typet::componentt::get_access
const irep_idt & get_access() const
Definition: std_types.h:93
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:443
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1009
vector_typet
The vector type.
Definition: std_types.h:969
struct_union_typet::componentt::get_pretty_name
const irep_idt & get_pretty_name() const
Definition: std_types.h:103
bool_typet
The Boolean type.
Definition: std_types.h:36
struct_union_typet::make_incomplete
void make_incomplete()
A struct/union may be incomplete.
Definition: std_types.h:185
struct_union_typet::default_access
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition: std_types.h:173
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
code_typet::parameter_indicest
std::unordered_map< irep_idt, std::size_t > parameter_indicest
Definition: std_types.h:701
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1034
can_cast_type< enumeration_typet >
bool can_cast_type< enumeration_typet >(const typet &type)
Check whether a reference to a typet is a enumeration_typet.
Definition: std_types.h:505
struct_union_typet::component_number
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:36
code_typet::remove_ellipsis
void remove_ellipsis()
Definition: std_types.h:634
struct_union_typet::componentt::set_name
void set_name(const irep_idt &name)
Definition: std_types.h:78
code_typet::get_is_constructor
bool get_is_constructor() const
Definition: std_types.h:679
code_typet::get_this
const parametert * get_this() const
Definition: std_types.h:615
struct_union_typet::components
componentst & components()
Definition: std_types.h:146
expr.h
array_typet::size
const exprt & size() const
Definition: std_types.h:765
string_typet::string_typet
string_typet()
Definition: std_types.h:876
struct_union_typet::struct_union_typet
struct_union_typet(const irep_idt &_id)
Definition: std_types.h:58
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
struct_union_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:166
can_cast_type< struct_typet >
bool can_cast_type< struct_typet >(const typet &type)
Check whether a reference to a typet is a struct_typet.
Definition: std_types.h:289
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:725
can_cast_type< vector_typet >
bool can_cast_type< vector_typet >(const typet &type)
Check whether a reference to a typet is a vector_typet.
Definition: std_types.h:981
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:162
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
struct_union_typet::struct_union_typet
struct_union_typet(const irep_idt &_id, componentst _components)
Definition: std_types.h:136
class_typet::static_memberst
componentst static_memberst
Definition: std_types.h:340
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:589
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:428
empty_typet
The empty type.
Definition: std_types.h:45
code_typet::get_access
const irep_idt & get_access() const
Definition: std_types.h:669
bitvector_typet::bitvector_typet
bitvector_typet(const irep_idt &_id, std::size_t width)
Definition: std_types.h:832
code_typet::parameter_identifiers
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition: std_types.h:690
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:73
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:163
can_cast_type< struct_tag_typet >
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:455
code_typet::set_is_constructor
void set_is_constructor()
Definition: std_types.h:684
code_typet::parametert::default_value
const exprt & default_value() const
Definition: std_types.h:556
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:156
struct_typet::struct_typet
struct_typet(componentst _components)
Definition: std_types.h:231
complex_typet::complex_typet
complex_typet(typet _subtype)
Definition: std_types.h:1011
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
struct_union_typet::componentt::get_is_padding
bool get_is_padding() const
Definition: std_types.h:123
struct_union_typet::componentt::set_pretty_name
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:108
can_cast_type< array_typet >
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition: std_types.h:794
code_typet::code_typet
code_typet(parameterst _parameters, typet _return_type)
Constructs a new code type, i.e., function type.
Definition: std_types.h:541
struct_union_typet::componentt::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:88
range_typet
A type for subranges of integers.
Definition: std_types.h:913
code_typet::set_inlined
void set_inlined(bool value)
Definition: std_types.h:664
class_typet::static_members
const static_memberst & static_members() const
Definition: std_types.h:342
struct_typet::is_class
bool is_class() const
A struct may be a class, where members may have access restrictions.
Definition: std_types.h:239
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:256
bitvector_typet::bitvector_typet
bitvector_typet(const irep_idt &_id)
Definition: std_types.h:828
irept::swap
void swap(irept &irep)
Definition: irep.h:453
code_typet
Base type of functions.
Definition: std_types.h:533
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:151
range_typet::get_to
mp_integer get_to() const
Definition: std_types.cpp:161
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
struct_typet::basest
std::vector< baset > basest
Definition: std_types.h:253
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:102
array_typet::size
exprt & size()
Definition: std_types.h:770
dstringt::empty
bool empty() const
Definition: dstring.h:88
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:390
enumeration_typet::enumeration_typet
enumeration_typet()
Definition: std_types.h:486
irept::baset
tree_implementationt baset
Definition: irep.h:385
bitvector_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:847
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
typet::check
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:100
class_typet::methodt
componentt methodt
Definition: std_types.h:326
can_cast_type< string_typet >
bool can_cast_type< string_typet >(const typet &type)
Check whether a reference to a typet is a string_typet.
Definition: std_types.h:885
code_typet::parametert::get_this
bool get_this() const
Definition: std_types.h:594
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:842
struct_union_typet::componentt::set_is_padding
void set_is_padding(bool is_padding)
Definition: std_types.h:128
struct_typet::bases
basest & bases()
Get the collection of base classes/structs.
Definition: std_types.h:262
code_typet::has_this
bool has_this() const
Definition: std_types.h:610
range_typet::range_typet
range_typet(const mp_integer &_from, const mp_integer &_to)
Definition: std_types.h:915
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:579
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:599
to_range_type
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:945
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
is_constant_or_has_constant_components
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:175
struct_union_typet::componentt
Definition: std_types.h:63
to_string_type
const string_typet & to_string_type(const typet &type)
Cast a typet to a string_typet.
Definition: std_types.h:898
enumeration_typet::elements
const irept::subt & elements() const
Definition: std_types.h:490
vector_typet::vector_typet
vector_typet(const typet &_subtype, const constant_exprt &_size)
Definition: std_types.cpp:237
range_typet::set_to
void set_to(const mp_integer &to)
Definition: std_types.cpp:151
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
struct_typet::struct_typet
struct_typet()
Definition: std_types.h:227
class_typet::methods
const methodst & methods() const
Definition: std_types.h:329
array_typet
Arrays with given size.
Definition: std_types.h:757
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
exprt::add_expr
exprt & add_expr(const irep_idt &name)
Definition: expr.h:309
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:826
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:629
code_typet::parametert::parametert
parametert(const typet &type)
Definition: std_types.h:552
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
can_cast_type< range_typet >
bool can_cast_type< range_typet >(const typet &type)
Check whether a reference to a typet is a range_typet.
Definition: std_types.h:932
string_typet
String type.
Definition: std_types.h:874
invariant.h
irept::set_size_t
void set_size_t(const irep_namet &name, const std::size_t value)
Definition: irep.cpp:93
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:584
irept::get_sub
subt & get_sub()
Definition: irep.h:467
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
code_typet::parametert
Definition: std_types.h:550
class_typet::class_typet
class_typet()
Definition: std_types.h:321
validate.h
code_typet::is_KnR
bool is_KnR() const
Definition: std_types.h:624
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:659
code_typet::return_type
typet & return_type()
Definition: std_types.h:644
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
array_typet::array_typet
array_typet(typet _subtype, exprt _size)
Definition: std_types.h:759
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:81
bool_typet::bool_typet
bool_typet()
Definition: std_types.h:38
enumeration_typet::elements
irept::subt & elements()
Definition: std_types.h:495
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
code_typet::parameter_indices
parameter_indicest parameter_indices() const
Get a map from parameter name to its index.
Definition: std_types.h:704
struct_union_typet::componentt::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:83
can_cast_type< class_typet >
bool can_cast_type< class_typet >(const typet &type)
Check whether a reference to a typet is a class_typet.
Definition: std_types.h:362
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
class_typet::methods
methodst & methods()
Definition: std_types.h:334
struct_union_typet::is_incomplete
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:179
can_cast_type< tag_typet >
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_typet.
Definition: std_types.h:414
can_cast_type< struct_union_typet >
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:195
code_typet::set_access
void set_access(const irep_idt &access)
Definition: std_types.h:674
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:860
code_typet::parameters
parameterst & parameters()
Definition: std_types.h:654
range_typet::set_from
void set_from(const mp_integer &_from)
Definition: std_types.cpp:146
code_typet::parametert::has_default_value
bool has_default_value() const
Definition: std_types.h:561
sharing_treet
Base class for tree-like data structures with sharing.
Definition: irep.h:168