File tree Expand file tree Collapse file tree 2 files changed +19
-0
lines changed Expand file tree Collapse file tree 2 files changed +19
-0
lines changed Original file line number Diff line number Diff line change @@ -289,3 +289,19 @@ require_type::require_java_non_generic_class(const typet &class_type)
289
289
290
290
return java_class_type;
291
291
}
292
+
293
+ // / Verify a given type is a symbol type, optionally with a specific identifier
294
+ // / \param type: The type to check
295
+ // / \param identifier: The identifier the symbol type should have
296
+ // / \return The cast version of the input type
297
+ const symbol_typet &
298
+ require_type::require_symbol (const typet &type, const irep_idt &identifier)
299
+ {
300
+ REQUIRE (type.id () == ID_symbol);
301
+ const symbol_typet &result = to_symbol_type (type);
302
+ if (identifier != " " )
303
+ {
304
+ REQUIRE (result.get_identifier () == identifier);
305
+ }
306
+ return result;
307
+ }
Original file line number Diff line number Diff line change @@ -25,6 +25,9 @@ namespace require_type
25
25
pointer_typet
26
26
require_pointer (const typet &type, const optionalt<typet> &subtype);
27
27
28
+ const symbol_typet &
29
+ require_symbol (const typet &type, const irep_idt &identifier = " " );
30
+
28
31
struct_typet::componentt require_component (
29
32
const struct_typet &struct_type,
30
33
const irep_idt &component_name);
You can’t perform that action at this time.
0 commit comments