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 struct_tag_typet &	require_struct_tag (const typet &type, const irep_idt &identifier="")
	Verify a given type is a symbol type, optionally with a specific identifier. More...

pointer_typet	require_pointer_to_tag (const typet &type, const irep_idt &identifier=irep_idt())

java_class_typet::componentt	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. 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...

java_method_typet	require_java_method (const typet &type)
	Checks a type is a java_method_typet (i.e. More...

code_typet::parametert	require_parameter (const code_typet &function_type, const irep_idt &param_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_method_typet	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. 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 &parameter)
	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< struct_tag_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_struct_tag_typet	require_java_generic_struct_tag_type (const typet &type, const std::string &identifier)
	Verify a given type is a java generic symbol type. More...

java_generic_struct_tag_typet	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. 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 Documentation

◆ expected_type_argumentst

typedef std::initializer_list<expected_type_argumentt> require_type::expected_type_argumentst

Definition at line 66 of file require_type.h.

◆ java_lambda_method_handlest

typedef java_class_typet::java_lambda_method_handlest require_type::java_lambda_method_handlest

Definition at line 131 of file require_type.h.

Enumeration Type Documentation

◆ type_argument_kindt

enum require_type::type_argument_kindt

strong

Enumerator
Inst
Var

Definition at line 55 of file require_type.h.

Function Documentation

◆ require_code() [1/2]

code_typet require_type::require_code ( const typet & type )

Checks a type is a code_type (i.e.

a function)

Parameters

type	The type to check

Returns: The cast version of the type code_type

Definition at line 72 of file require_type.cpp.

◆ require_code() [2/2]

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.

Parameters

type	The type to check
num_params	check the the given code_typet expects this number of parameters

Returns: The type cast to a code_typet

Definition at line 85 of file require_type.cpp.

◆ require_complete_class()

class_typet require_type::require_complete_class ( const typet & class_type )

Checks that the given type is a complete class.

Parameters

class_type type of the class

Returns: class_type of the class

Definition at line 258 of file require_type.cpp.

◆ require_complete_java_generic_class() [1/2]

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.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 336 of file require_type.cpp.

◆ require_complete_java_generic_class() [2/2]

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.

Parameters

class_type	the class
type_variables	vector of type variables

Returns: A reference to the java generic class type.

Definition at line 347 of file require_type.cpp.

◆ require_complete_java_implicitly_generic_class() [1/2]

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.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 407 of file require_type.cpp.

◆ require_complete_java_implicitly_generic_class() [2/2]

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.

Parameters

class_type	the class
implicit_type_variables	vector of type variables

Returns: A reference to the java generic class type.

Definition at line 420 of file require_type.cpp.

◆ require_complete_java_non_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.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 451 of file require_type.cpp.

◆ require_component() [1/2]

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.

Parameters

java_class_type	The class that should have the component
component_name	The name of the component

Returns: The component with the specified name

Definition at line 35 of file require_type.cpp.

◆ require_component() [2/2]

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.

Parameters

struct_type	The structure that should have the component
component_name	The name of the component

Returns: The component with the specified name

Definition at line 54 of file require_type.cpp.

◆ require_incomplete_class()

class_typet require_type::require_incomplete_class ( const typet & class_type )

Checks that the given type is an incomplete class.

Parameters

class_type type of the class

Returns: class_type of the class

Definition at line 272 of file require_type.cpp.

◆ require_java_generic_class() [1/2]

java_generic_class_typet require_type::require_java_generic_class ( const typet & class_type )

Verify that a class is a valid java generic class.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 287 of file require_type.cpp.

◆ require_java_generic_class() [2/2]

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.

Parameters

class_type	the class
type_variables	vector of type variables

Returns: A reference to the java generic class type.

Definition at line 307 of file require_type.cpp.

◆ require_java_generic_parameter() [1/2]

java_generic_parametert require_type::require_java_generic_parameter ( const typet & type )

Verify a given type is a java_generic_parameter, e.g., T

Parameters

type	The type to check

Returns: The type, cast to a java_generic_parametert

Definition at line 213 of file require_type.cpp.

◆ require_java_generic_parameter() [2/2]

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")

Parameters

type	The type to check
parameter	String with the parameter name.

Returns: The given type, cast to a java_generic_parametert

Definition at line 225 of file require_type.cpp.

◆ require_java_generic_struct_tag_type() [1/2]

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.

Parameters

type	The type to check
identifier	The identifier to match

Returns: The type, cast to a java_generic_struct_tag_typet

Definition at line 486 of file require_type.cpp.

◆ require_java_generic_struct_tag_type() [2/2]

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.

Expected usage is something like this:

require_java_generic_struct_tag_type(type, "java::Generic", {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}, {require_type::type_argument_kindt::Var, "T"}})

Parameters

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

Returns: The given type, cast to a java_generic_struct_tag_typet

Definition at line 509 of file require_type.cpp.

◆ require_java_generic_type() [1/2]

java_generic_typet require_type::require_java_generic_type ( const typet & type )

Verify a given type is a java_generic_type.

Parameters

type	The type to check

Returns: The type, cast to a java_generic_typet

Definition at line 171 of file require_type.cpp.

◆ require_java_generic_type() [2/2]

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"}})

Parameters

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.

Returns: The given type, cast to a java_generic_typet

Definition at line 189 of file require_type.cpp.

◆ require_java_implicitly_generic_class() [1/2]

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.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 359 of file require_type.cpp.

◆ require_java_implicitly_generic_class() [2/2]

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.

Parameters

class_type	the class
implicit_type_variables	vector of type variables

Returns: A reference to the java generic class type.

Definition at line 381 of file require_type.cpp.

◆ require_java_method() [1/2]

java_method_typet require_type::require_java_method ( const typet & type )

Checks a type is a java_method_typet (i.e.

a function)

Parameters

type	The type to check

Returns: The cast version of the type method_type

Definition at line 95 of file require_type.cpp.

◆ require_java_method() [2/2]

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.

Parameters

type	The type to check
num_params	check the the given java_method_typet expects this number of parameters

Returns: The type cast to a java_method_typet

Definition at line 108 of file require_type.cpp.

◆ require_java_non_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.

Parameters

class_type the class

Returns: A reference to the java generic class type.

Definition at line 433 of file require_type.cpp.

◆ require_java_non_generic_type()

const typet & require_type::require_java_non_generic_type	(	const typet &	type,
		const optionalt< struct_tag_typet > &	expect_subtype
	)

Test a type to ensure it is not a java generics type.

Parameters

type	The type to test
expect_subtype	Optionally, also test that the subtype of the given type matches this parameter

Returns: The value passed in the first argument

Definition at line 244 of file require_type.cpp.

◆ require_lambda_method_handles()

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.

Parameters

class_type	class type to be verified
expected_identifiers	expected list of lambda method handle references

Returns: lambda method handles of the class

Definition at line 537 of file require_type.cpp.

◆ require_parameter()

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.

Parameters

function_type	The type of the function
param_name	The name of the parameter

Returns: A reference to the parameter structure corresponding to this parameter name.

Definition at line 120 of file require_type.cpp.

◆ require_pointer()

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.

Parameters

type	The type to check
subtype	An optional subtype. If provided, checks the subtype of the pointer is this.

Returns: A cast to pointer_typet version of type

Definition at line 18 of file require_type.cpp.

◆ require_pointer_to_tag()

pointer_typet require_type::require_pointer_to_tag	(	const typet &	type,
		const irep_idt &	identifier = `irep_idt()`
	)

Definition at line 474 of file require_type.cpp.

◆ require_struct_tag()

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.

Parameters

type	The type to check
identifier	The identifier the symbol type should have

Returns: The cast version of the input type

Definition at line 462 of file require_type.cpp.

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ expected_type_argumentst

◆ java_lambda_method_handlest

Enumeration Type Documentation

◆ type_argument_kindt

Function Documentation

◆ require_code() [1/2]

◆ require_code() [2/2]

◆ require_complete_class()

◆ require_complete_java_generic_class() [1/2]

◆ require_complete_java_generic_class() [2/2]

◆ require_complete_java_implicitly_generic_class() [1/2]

◆ require_complete_java_implicitly_generic_class() [2/2]

◆ require_complete_java_non_generic_class()

◆ require_component() [1/2]

◆ require_component() [2/2]

◆ require_incomplete_class()

◆ require_java_generic_class() [1/2]

◆ require_java_generic_class() [2/2]

◆ require_java_generic_parameter() [1/2]

◆ require_java_generic_parameter() [2/2]

◆ require_java_generic_struct_tag_type() [1/2]

◆ require_java_generic_struct_tag_type() [2/2]

◆ require_java_generic_type() [1/2]

◆ require_java_generic_type() [2/2]

◆ require_java_implicitly_generic_class() [1/2]

◆ require_java_implicitly_generic_class() [2/2]

◆ require_java_method() [1/2]

◆ require_java_method() [2/2]

◆ require_java_non_generic_class()

◆ require_java_non_generic_type()

◆ require_lambda_method_handles()

◆ require_parameter()

◆ require_pointer()

◆ require_pointer_to_tag()

◆ require_struct_tag()