cprover
type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines typet, type_with_subtypet and type_with_subtypest
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_TYPE_H
14 #define CPROVER_UTIL_TYPE_H
15 
16 class namespacet;
17 
18 #include "source_location.h"
19 #include "validate_types.h"
20 #include "validation_mode.h"
21 
27 class typet:public irept
28 {
29 public:
30  typet() { }
31 
32  explicit typet(const irep_idt &_id):irept(_id) { }
33 
34  // the STL implementation shipped with GCC 5 is broken
35 #if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
36  typet(irep_idt _id, typet _subtype)
37  : irept(std::move(_id), {}, {std::move(_subtype)})
38  {
39  }
40 #else
41  typet(irep_idt _id, typet _subtype) : irept(std::move(_id))
42  {
43  subtype() = std::move(_subtype);
44  }
45 #endif
46 
47  const typet &subtype() const
48  {
49  if(get_sub().empty())
50  return static_cast<const typet &>(get_nil_irep());
51  return static_cast<const typet &>(get_sub().front());
52  }
53 
55  {
56  subt &sub=get_sub();
57  if(sub.empty())
58  sub.resize(1);
59  return static_cast<typet &>(sub.front());
60  }
61 
62  bool has_subtypes() const
63  { return !get_sub().empty(); }
64 
65  bool has_subtype() const
66  { return !get_sub().empty(); }
67 
69  { get_sub().clear(); }
70 
72  {
73  return (const source_locationt &)find(ID_C_source_location);
74  }
75 
77  {
78  return static_cast<source_locationt &>(add(ID_C_source_location));
79  }
80 
81  typet &add_type(const irep_namet &name)
82  {
83  return static_cast<typet &>(add(name));
84  }
85 
86  const typet &find_type(const irep_namet &name) const
87  {
88  return static_cast<const typet &>(find(name));
89  }
90 
99  static void
101  {
102  }
103 
112  static void validate(
113  const typet &type,
114  const namespacet &,
116  {
117  check_type(type, vm);
118  }
119 
128  static void validate_full(
129  const typet &type,
130  const namespacet &ns,
132  {
133  // check subtypes
134  for(const irept &sub : type.get_sub())
135  {
136  const typet &subtype = static_cast<const typet &>(sub);
137  validate_full_type(subtype, ns, vm);
138  }
139 
140  validate_type(type, ns, vm);
141  }
142 };
143 
146 {
147 public:
149  : typet(std::move(_id), std::move(_subtype))
150  {
151  }
152 };
153 
155 {
156  PRECONDITION(type.has_subtype());
157  return static_cast<const type_with_subtypet &>(type);
158 }
159 
161 {
162  PRECONDITION(type.has_subtype());
163  return static_cast<type_with_subtypet &>(type);
164 }
165 
168 {
169 public:
170  typedef std::vector<typet> subtypest;
171 
172  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
173  : typet(_id)
174  {
175  subtypes() = _subtypes;
176  }
177 
178  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
179  {
180  subtypes() = std::move(_subtypes);
181  }
182 
184  {
185  return (subtypest &)get_sub();
186  }
187 
188  const subtypest &subtypes() const
189  {
190  return (const subtypest &)get_sub();
191  }
192 
193  void move_to_subtypes(typet &type); // destroys type
194 
195  void copy_to_subtypes(const typet &type);
196 };
197 
199 {
200  return static_cast<const type_with_subtypest &>(type);
201 }
202 
204 {
205  return static_cast<type_with_subtypest &>(type);
206 }
207 
210 typet remove_const(typet type);
211 
212 #endif // CPROVER_UTIL_TYPE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
type_with_subtypest::copy_to_subtypes
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
Definition: type.cpp:17
typet::subtype
const typet & subtype() const
Definition: type.h:47
type_with_subtypest
Type with multiple subtypes.
Definition: type.h:168
type_with_subtypest::subtypest
std::vector< typet > subtypest
Definition: type.h:170
validate_full_type
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
Definition: validate_types.cpp:110
typet
The type of an expression, extends irept.
Definition: type.h:28
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
typet::has_subtypes
bool has_subtypes() const
Definition: type.h:62
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
type_with_subtypest::subtypes
subtypest & subtypes()
Definition: type.h:183
typet::typet
typet()
Definition: type.h:30
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
type_with_subtypest::type_with_subtypest
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:172
check_type
void check_type(const typet &type, const validation_modet vm)
Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: validate_types.cpp:81
type_with_subtypet::type_with_subtypet
type_with_subtypet(irep_idt _id, typet _subtype)
Definition: type.h:148
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
type_with_subtypest::move_to_subtypes
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition: type.cpp:25
source_location.h
typet::remove_subtype
void remove_subtype()
Definition: type.h:68
validation_modet
validation_modet
Definition: validation_mode.h:13
validation_mode.h
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
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
typet::validate
static void validate(const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed, assuming that its subtypes have already been checked for well-for...
Definition: type.h:112
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
source_locationt
Definition: source_location.h:20
typet::validate_full
static void validate_full(const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the type is well-formed (full check, including checks of subtypes)
Definition: type.h:128
type_with_subtypest::subtypes
const subtypest & subtypes() const
Definition: type.h:188
typet::typet
typet(irep_idt _id, typet _subtype)
Definition: type.h:36
validate_type
void validate_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed, assuming that its subtypes have already been checked for we...
Definition: validate_types.cpp:94
irept::get_sub
subt & get_sub()
Definition: irep.h:467
remove_const
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:81
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
validate_types.h
typet::subtype
typet & subtype()
Definition: type.h:54
typet::typet
typet(const irep_idt &_id)
Definition: type.h:32
type_with_subtypest::type_with_subtypest
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Definition: type.h:178