Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression.  
More...
 | 
| pointer_typet  | require_type::require_pointer (const typet &type, const std::optional< typet > &subtype) | 
|   | Checks a type is a pointer type optionally with a specific subtype.  
  | 
|   | 
| const struct_tag_typet &  | require_type::require_struct_tag (const typet &type, const irep_idt &identifier="") | 
|   | Verify a given type is a symbol type, optionally with a specific identifier.  
  | 
|   | 
| pointer_typet  | require_type::require_pointer_to_tag (const typet &type, const irep_idt &identifier=irep_idt()) | 
|   | 
| java_class_typet::componentt  | require_type::require_component (const java_class_typet &java_class_type, const irep_idt &component_name) | 
|   | Checks that a class has a component with a specific name.  
  | 
|   | 
| struct_typet::componentt  | require_type::require_component (const struct_typet &struct_type, const irep_idt &component_name) | 
|   | Checks a struct like type has a component with a specific name.  
  | 
|   | 
| code_typet  | require_type::require_code (const typet &type) | 
|   | Checks a type is a code_type (i.e.  
  | 
|   | 
| java_method_typet  | require_type::require_java_method (const typet &type) | 
|   | Checks a type is a java_method_typet (i.e.  
  | 
|   | 
| code_typet::parametert  | require_type::require_parameter (const code_typet &function_type, const irep_idt ¶m_name) | 
|   | Verify that a function has a parameter of a specific name.  
  | 
|   | 
| code_typet  | require_type::require_code (const typet &type, const size_t num_params) | 
|   | Verify a given type is an code_typet, and that the code it represents accepts a given number of parameters.  
  | 
|   | 
| java_method_typet  | require_type::require_java_method (const typet &type, const size_t num_params) | 
|   | Verify a given type is an java_method_typet, and that the code it represents accepts a given number of parameters.  
  | 
|   | 
| java_generic_typet  | require_type::require_java_generic_type (const typet &type) | 
|   | Verify a given type is a java_generic_type.  
  | 
|   | 
| java_generic_typet  | require_type::require_java_generic_type (const typet &type, const require_type::expected_type_argumentst &type_expectations) | 
|   | Verify a given type is a java_generic_type, checking that it's associated type arguments match a given set of identifiers.  
  | 
|   | 
| java_generic_parametert  | require_type::require_java_generic_parameter (const typet &type) | 
|   | Verify a given type is a java_generic_parameter, e.g., T  
  | 
|   | 
| java_generic_parametert  | require_type::require_java_generic_parameter (const typet &type, const irep_idt ¶meter) | 
|   | Verify a given type is a java_generic_parametert with the given name.  
  | 
|   | 
| const typet &  | require_type::require_java_non_generic_type (const typet &type, const std::optional< struct_tag_typet > &expect_subtype) | 
|   | Test a type to ensure it is not a java generics type.  
  | 
|   | 
| class_typet  | require_type::require_complete_class (const typet &class_type) | 
|   | Checks that the given type is a complete class.  
  | 
|   | 
| class_typet  | require_type::require_incomplete_class (const typet &class_type) | 
|   | Checks that the given type is an incomplete class.  
  | 
|   | 
| java_generic_class_typet  | require_type::require_java_generic_class (const typet &class_type) | 
|   | Verify that a class is a valid java generic class.  
  | 
|   | 
| java_generic_class_typet  | require_type::require_java_generic_class (const typet &class_type, const std::initializer_list< irep_idt > &type_variables) | 
|   | Verify that a class is a valid java generic class with the specified list of variables.  
  | 
|   | 
| java_generic_class_typet  | require_type::require_complete_java_generic_class (const typet &class_type) | 
|   | Verify that a class is a complete, valid java generic class.  
  | 
|   | 
| java_generic_class_typet  | require_type::require_complete_java_generic_class (const typet &class_type, const std::initializer_list< irep_idt > &type_parameters) | 
|   | Verify that a class is a complete, valid java generic class with the specified list of variables.  
  | 
|   | 
| java_implicitly_generic_class_typet  | require_type::require_java_implicitly_generic_class (const typet &class_type) | 
|   | Verify that a class is a valid java implicitly generic class.  
  | 
|   | 
| java_implicitly_generic_class_typet  | require_type::require_java_implicitly_generic_class (const typet &class_type, const std::initializer_list< irep_idt > &implicit_type_variables) | 
|   | Verify that a class is a valid java generic class with the specified list of variables.  
  | 
|   | 
| java_implicitly_generic_class_typet  | require_type::require_complete_java_implicitly_generic_class (const typet &class_type) | 
|   | Verify that a class is a complete, valid java implicitly generic class.  
  | 
|   | 
| java_implicitly_generic_class_typet  | require_type::require_complete_java_implicitly_generic_class (const typet &class_type, const std::initializer_list< irep_idt > &implicit_type_variables) | 
|   | Verify that a class is a complete, valid java generic class with the specified list of variables.  
  | 
|   | 
| java_class_typet  | require_type::require_java_non_generic_class (const typet &class_type) | 
|   | Verify that a class is a valid nongeneric java class.  
  | 
|   | 
| java_class_typet  | require_type::require_complete_java_non_generic_class (const typet &class_type) | 
|   | Verify that a class is a complete, valid nongeneric java class.  
  | 
|   | 
| java_generic_struct_tag_typet  | require_type::require_java_generic_struct_tag_type (const typet &type, const std::string &identifier) | 
|   | Verify a given type is a java generic symbol type.  
  | 
|   | 
| java_generic_struct_tag_typet  | require_type::require_java_generic_struct_tag_type (const typet &type, const std::string &identifier, const require_type::expected_type_argumentst &type_expectations) | 
|   | Verify a given type is a java generic symbol type, checking that it's associated type arguments match a given set of identifiers.  
  | 
|   | 
| java_lambda_method_handlest  | require_type::require_lambda_method_handles (const java_class_typet &class_type, const std::vector< std::string > &expected_identifiers) | 
|   | Verify that the lambda method handles of a class match the given expectation.  
  | 
|   | 
Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression. 
Definition in file require_type.h.