|
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