cprover
|
Classes | |
struct | expected_type_argumentt |
Typedefs | |
typedef std::initializer_list< expected_type_argumentt > | expected_type_argumentst |
typedef java_class_typet::java_lambda_method_handlest | java_lambda_method_handlest |
Enumerations | |
enum | type_argument_kindt { type_argument_kindt::Inst, type_argument_kindt::Var } |
Functions | |
pointer_typet | require_pointer (const typet &type, const optionalt< typet > &subtype) |
Checks a type is a pointer type optionally with a specific subtype. More... | |
const symbol_typet & | require_symbol (const typet &type, const irep_idt &identifier="") |
Verify a given type is a symbol type, optionally with a specific identifier. More... | |
struct_typet::componentt | require_component (const struct_typet &struct_type, const irep_idt &component_name) |
Checks a struct like type has a component with a specific name. More... | |
code_typet | require_code (const typet &type) |
Checks a type is a code_type (i.e. More... | |
code_typet::parametert | require_parameter (const code_typet &function_type, const irep_idt ¶m_name) |
Verify that a function has a parameter of a specific name. More... | |
code_typet | 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. More... | |
java_generic_typet | require_java_generic_type (const typet &type) |
Verify a given type is a java_generic_type. More... | |
java_generic_typet | 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. More... | |
java_generic_parametert | require_java_generic_parameter (const typet &type) |
Verify a given type is a java_generic_parameter, e.g., T More... | |
java_generic_parametert | require_java_generic_parameter (const typet &type, const irep_idt ¶meter) |
Verify a given type is a java_generic_parametert with the given name. More... | |
const typet & | require_java_non_generic_type (const typet &type, const optionalt< symbol_typet > &expect_subtype) |
Test a type to ensure it is not a java generics type. More... | |
class_typet | require_complete_class (const typet &class_type) |
Checks that the given type is a complete class. More... | |
class_typet | require_incomplete_class (const typet &class_type) |
Checks that the given type is an incomplete class. More... | |
java_generic_class_typet | require_java_generic_class (const typet &class_type) |
Verify that a class is a valid java generic class. More... | |
java_generic_class_typet | 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. More... | |
java_generic_class_typet | require_complete_java_generic_class (const typet &class_type) |
Verify that a class is a complete, valid java generic class. More... | |
java_generic_class_typet | 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. More... | |
java_implicitly_generic_class_typet | require_java_implicitly_generic_class (const typet &class_type) |
Verify that a class is a valid java implicitly generic class. More... | |
java_implicitly_generic_class_typet | 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. More... | |
java_implicitly_generic_class_typet | require_complete_java_implicitly_generic_class (const typet &class_type) |
Verify that a class is a complete, valid java implicitly generic class. More... | |
java_implicitly_generic_class_typet | 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. More... | |
java_class_typet | require_java_non_generic_class (const typet &class_type) |
Verify that a class is a valid nongeneric java class. More... | |
java_class_typet | require_complete_java_non_generic_class (const typet &class_type) |
Verify that a class is a complete, valid nongeneric java class. More... | |
java_generic_symbol_typet | require_java_generic_symbol_type (const typet &type, const std::string &identifier) |
Verify a given type is a java generic symbol type. More... | |
java_generic_symbol_typet | require_java_generic_symbol_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. More... | |
java_lambda_method_handlest | 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. More... | |
typedef std::initializer_list<expected_type_argumentt> require_type::expected_type_argumentst |
Definition at line 55 of file require_type.h.
Definition at line 120 of file require_type.h.
|
strong |
Enumerator | |
---|---|
Inst | |
Var |
Definition at line 44 of file require_type.h.
code_typet require_type::require_code | ( | const typet & | type | ) |
Checks a type is a code_type (i.e.
a function)
type | The type to check |
Definition at line 56 of file require_type.cpp.
References irept::id(), and to_code_type().
Referenced by require_code().
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.
type | The type to check |
num_params | check the the given code_typet expects this number of parameters |
Definition at line 69 of file require_type.cpp.
References code_typet::parameters(), and require_code().
class_typet require_type::require_complete_class | ( | const typet & | class_type | ) |
Checks that the given type is a complete class.
class_type | type of the class |
Definition at line 217 of file require_type.cpp.
References irept::id(), and to_class_type().
Referenced by require_complete_java_generic_class(), require_complete_java_implicitly_generic_class(), and require_complete_java_non_generic_class().
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.
class_type | the class |
Definition at line 295 of file require_type.cpp.
References require_complete_class(), and require_java_generic_class().
Referenced by require_complete_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_variables | ||
) |
Verify that a class is a complete, valid java generic class with the specified list of variables.
class_type | the class |
type_variables | vector of type variables |
Definition at line 306 of file require_type.cpp.
References require_complete_java_generic_class(), and require_java_generic_class().
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.
class_type | the class |
Definition at line 371 of file require_type.cpp.
References require_complete_class(), and require_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.
class_type | the class |
type_variables | vector of type variables |
Definition at line 384 of file require_type.cpp.
References require_complete_class(), and require_java_implicitly_generic_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.
class_type | the class |
Definition at line 415 of file require_type.cpp.
References require_complete_class(), and require_java_non_generic_class().
struct_union_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.
struct_type | The structure that should have the component |
component_name | The name of the component |
Definition at line 38 of file require_type.cpp.
References struct_union_typet::components().
class_typet require_type::require_incomplete_class | ( | const typet & | class_type | ) |
Checks that the given type is an incomplete class.
class_type | type of the class |
Definition at line 231 of file require_type.cpp.
References irept::id(), and to_class_type().
java_generic_class_typet require_type::require_java_generic_class | ( | const typet & | class_type | ) |
Verify that a class is a valid java generic class.
class_type | the class |
Definition at line 246 of file require_type.cpp.
References irept::id(), is_java_generic_class_type(), to_class_type(), to_java_class_type(), and to_java_generic_class_type().
Referenced by require_complete_java_generic_class(), and require_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.
class_type | the class |
type_variables | vector of type variables |
Definition at line 266 of file require_type.cpp.
References java_generic_class_typet::generic_types(), is_java_generic_parameter(), and require_java_generic_class().
java_generic_parametert require_type::require_java_generic_parameter | ( | const typet & | type | ) |
Verify a given type is a java_generic_parameter, e.g., T
type | The type to check |
Definition at line 172 of file require_type.cpp.
References is_java_generic_parameter(), and to_java_generic_parameter().
Referenced by require_java_generic_parameter().
java_generic_parametert require_type::require_java_generic_parameter | ( | const typet & | type, |
const irep_idt & | parameter | ||
) |
Verify a given type is a java_generic_parametert with the given name.
Expected usage is something like this: require_java_generic_parameter(parameter, "java::Generic::T")
type | The type to check |
parameter | String with the parameter name. |
Definition at line 184 of file require_type.cpp.
References require_java_generic_parameter(), require_java_generic_type_argument_expectation(), and Var.
java_generic_symbol_typet require_type::require_java_generic_symbol_type | ( | const typet & | type, |
const std::string & | identifier | ||
) |
Verify a given type is a java generic symbol type.
type | The type to check |
identifier | The identifier to match |
Definition at line 441 of file require_type.cpp.
References is_java_generic_symbol_type(), require_expr::require_symbol(), and to_java_generic_symbol_type().
Referenced by require_java_generic_symbol_type().
java_generic_symbol_typet require_type::require_java_generic_symbol_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.
Expected usage is something like this:
require_java_generic_symbol_type(type, "java::Generic", {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}, {require_type::type_argument_kindt::Var, "T"}})
type | The type to check |
identifier | The identifier to match |
type_expectations | A set of type argument kinds and identifiers which should be expected as the type arguments of the given generic type |
Definition at line 463 of file require_type.cpp.
References java_generic_symbol_typet::generic_types(), require_java_generic_symbol_type(), and require_java_generic_type_argument_expectation().
java_generic_typet require_type::require_java_generic_type | ( | const typet & | type | ) |
Verify a given type is a java_generic_type.
type | The type to check |
Definition at line 130 of file require_type.cpp.
References is_java_generic_type(), and to_java_generic_type().
Referenced by require_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.
Expected usage is something like this:
require_java_generic_type(type, {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}, {require_type::type_argument_kindt::Var, "T"}})
type | The type to check |
type_expectations | A set of type argument kinds and identifiers which should be expected as the type arguments of the given generic type. |
Definition at line 148 of file require_type.cpp.
References java_generic_typet::generic_type_arguments(), require_java_generic_type(), and require_java_generic_type_argument_expectation().
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.
class_type | the class |
Definition at line 318 of file require_type.cpp.
References irept::id(), is_java_implicitly_generic_class_type(), to_class_type(), to_java_class_type(), and to_java_implicitly_generic_class_type().
Referenced by require_complete_java_implicitly_generic_class(), and require_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.
class_type | the class |
type_variables | vector of type variables |
Definition at line 340 of file require_type.cpp.
References java_implicitly_generic_class_typet::implicit_generic_types(), is_java_generic_parameter(), and require_java_implicitly_generic_class().
java_class_typet require_type::require_java_non_generic_class | ( | const typet & | class_type | ) |
Verify that a class is a valid nongeneric java class.
class_type | the class |
Definition at line 397 of file require_type.cpp.
References irept::id(), is_java_generic_class_type(), is_java_implicitly_generic_class_type(), to_class_type(), and to_java_class_type().
Referenced by require_complete_java_non_generic_class().
const typet & require_type::require_java_non_generic_type | ( | const typet & | type, |
const optionalt< symbol_typet > & | expect_subtype | ||
) |
Test a type to ensure it is not a java generics type.
type | The type to test |
expect_subtype | Optionally, also test that the subtype of the given type matches this parameter |
Definition at line 203 of file require_type.cpp.
References is_java_generic_parameter(), is_java_generic_type(), and typet::subtype().
require_type::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.
class_struct | class type to be verified |
expected_identifiers | expected list of lambda method handle references |
Definition at line 491 of file require_type.cpp.
References symbol_exprt::get_identifier(), and java_class_typet::lambda_method_handles().
code_typet::parametert require_type::require_parameter | ( | const code_typet & | function_type, |
const irep_idt & | param_name | ||
) |
Verify that a function has a parameter of a specific name.
function_type | The type of the function |
param_name | The name of the parameter |
Definition at line 81 of file require_type.cpp.
References code_typet::parameters().
pointer_typet require_type::require_pointer | ( | const typet & | type, |
const optionalt< typet > & | subtype | ||
) |
Checks a type is a pointer type optionally with a specific subtype.
type | The type to check |
subtype | An optional subtype. If provided, checks the subtype of the pointer is this. |
Definition at line 19 of file require_type.cpp.
References irept::id(), and to_pointer_type().
const symbol_typet & require_type::require_symbol | ( | const typet & | type, |
const irep_idt & | identifier = "" |
||
) |
Verify a given type is a symbol type, optionally with a specific identifier.
type | The type to check |
identifier | The identifier the symbol type should have |
Definition at line 426 of file require_type.cpp.
References irept::id(), and to_symbol_type().