@@ -13,7 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com
13
13
#ifndef CPROVER_UTIL_TYPE_H
14
14
#define CPROVER_UTIL_TYPE_H
15
15
16
+ class namespacet ;
17
+
16
18
#include " source_location.h"
19
+ #include " validate.h"
20
+ #include " validate_types.h"
17
21
18
22
// / The type of an expression, extends irept. Types may have subtypes. This is
19
23
// / modeled with two subs named “subtype” (a single type) and “subtypes”
@@ -74,6 +78,55 @@ class typet:public irept
74
78
{
75
79
return static_cast <const typet &>(find (name));
76
80
}
81
+
82
+ // / Check that the type is well-formed (shallow checks only, i.e., subtypes
83
+ // / are not checked)
84
+ // /
85
+ // / Subclasses may override this method to provide specific well-formedness
86
+ // / checks for the corresponding types.
87
+ // /
88
+ // / The validation mode indicates whether well-formedness check failures are
89
+ // / reported via DATA_INVARIANT violations or exceptions.
90
+ void check (const validation_modet vm = validation_modet::INVARIANT) const
91
+ {
92
+ }
93
+
94
+ // / Check that the type is well-formed, assuming that its subtypes have
95
+ // / already been checked for well-formedness.
96
+ // /
97
+ // / Subclasses may override this method to provide specific well-formedness
98
+ // / checks for the corresponding types.
99
+ // /
100
+ // / The validation mode indicates whether well-formedness check failures are
101
+ // / reported via DATA_INVARIANT violations or exceptions.
102
+ void validate (
103
+ const namespacet &ns,
104
+ const validation_modet vm = validation_modet::INVARIANT) const
105
+ {
106
+ check_type_pick (*this , vm);
107
+ }
108
+
109
+ // / Check that the type is well-formed (full check, including checks of
110
+ // / subtypes)
111
+ // /
112
+ // / Subclasses may override this method, though in most cases the provided
113
+ // / implementation should be sufficient.
114
+ // /
115
+ // / The validation mode indicates whether well-formedness check failures are
116
+ // / reported via DATA_INVARIANT violations or exceptions.
117
+ void validate_full (
118
+ const namespacet &ns,
119
+ const validation_modet vm = validation_modet::INVARIANT) const
120
+ {
121
+ // check subtypes
122
+ for (const irept &sub : get_sub ())
123
+ {
124
+ const typet &subtype = static_cast <const typet &>(sub);
125
+ validate_type_full_pick (subtype, ns, vm);
126
+ }
127
+
128
+ validate_type_pick (*this , ns, vm);
129
+ }
77
130
};
78
131
79
132
// / Type with a single subtype.
0 commit comments