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)
289289
290290 return java_class_type;
291291}
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
2525pointer_typet
2626require_pointer (const typet &type, const optionalt<typet> &subtype);
2727
28+ const symbol_typet &
29+ require_symbol (const typet &type, const irep_idt &identifier = " " );
30+
2831struct_typet::componentt require_component (
2932 const struct_typet &struct_type,
3033 const irep_idt &component_name);
You can’t perform that action at this time.
0 commit comments