CBMC
java_types.h File Reference
#include <util/invariant.h>
#include <algorithm>
#include <set>
#include <util/c_types.h>
#include <util/narrow.h>
#include <util/std_expr.h>
+ Include dependency graph for java_types.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  java_annotationt
 
class  java_annotationt::valuet
 
class  annotated_typet
 
class  java_method_typet
 
class  java_class_typet
 
class  java_class_typet::componentt
 
class  java_class_typet::methodt
 
class  java_class_typet::java_lambda_method_handlet
 Represents a lambda call to a method. More...
 
class  java_reference_typet
 This is a specialization of reference_typet. More...
 
class  java_generic_parameter_tagt
 Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>. More...
 
class  java_generic_parametert
 Reference that points to a java_generic_parameter_tagt. More...
 
class  java_generic_struct_tag_typet
 Class to hold type with generic type arguments, for example java.util.List in either a reference of type List<Integer> or List<T> (here T must have been concretized already to create this object so technically it is an argument rather than parameter/variable, but in the symbol table this still shows as the parameter T). More...
 
class  java_generic_typet
 Reference that points to a java_generic_struct_tag_typet. More...
 
class  java_generic_class_typet
 Class to hold a class with generics, extends the java class type with a vector of java generic type parameters (also called type variables). More...
 
class  java_implicitly_generic_class_typet
 Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class or a derived class of a generic base class. More...
 
class  unsupported_java_class_signature_exceptiont
 An exception that is raised for unsupported class signature. More...
 

Macros

#define JAVA_REFERENCE_ARRAY_CLASSID   "java::array[reference]"
 
#define JAVA_ARRAY_DIMENSION_FIELD_NAME   "@array_dimensions"
 
#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME   "@element_class_identifier"
 

Functions

const annotated_typetto_annotated_type (const typet &type)
 
annotated_typetto_annotated_type (typet &type)
 
template<>
bool can_cast_type< annotated_typet > (const typet &)
 
template<>
bool can_cast_type< java_method_typet > (const typet &type)
 
const java_method_typetto_java_method_type (const typet &type)
 
java_method_typetto_java_method_type (typet &type)
 
const java_class_typetto_java_class_type (const typet &type)
 
java_class_typetto_java_class_type (typet &type)
 
template<>
bool can_cast_type< java_class_typet > (const typet &type)
 
template<>
bool can_cast_type< java_reference_typet > (const typet &type)
 
const java_reference_typetto_java_reference_type (const typet &type)
 
java_reference_typetto_java_reference_type (typet &type)
 
signedbv_typet java_int_type ()
 
signedbv_typet java_long_type ()
 
signedbv_typet java_short_type ()
 
signedbv_typet java_byte_type ()
 
unsignedbv_typet java_char_type ()
 
floatbv_typet java_float_type ()
 
floatbv_typet java_double_type ()
 
c_bool_typet java_boolean_type ()
 
empty_typet java_void_type ()
 
java_reference_typet java_reference_type (const struct_tag_typet &subtype)
 
reference_typet java_reference_type (const typet &subtype)
 
java_reference_typet java_lang_object_type ()
 
struct_tag_typet java_classname (const std::string &)
 
java_reference_typet java_array_type (const char subtype)
 Construct an array pointer type. More...
 
java_reference_typet java_reference_array_type (const struct_tag_typet &element_type)
 
const typetjava_array_element_type (const struct_tag_typet &array_symbol)
 Return a const reference to the element type of a given java array type. More...
 
typetjava_array_element_type (struct_tag_typet &array_symbol)
 Return a non-const reference to the element type of a given java array type. More...
 
bool is_java_array_type (const typet &type)
 Checks whether the given type is an array pointer type. More...
 
bool is_multidim_java_array_type (const typet &type)
 Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array type with element type also being a pointer to an array type. More...
 
std::pair< typet, std::size_t > java_array_dimension_and_element_type (const struct_tag_typet &type)
 Returns the underlying element type and array dimensionality of Java struct type. More...
 
exprt get_array_dimension_field (const exprt &pointer)
 
exprt get_array_element_type_field (const exprt &pointer)
 
typet java_type_from_char (char t)
 Constructs a type indicated by the given character: More...
 
std::optional< typetjava_type_from_string (const std::string &, const std::string &class_name_prefix="")
 Transforms a string representation of a Java type into an internal type representation thereof. More...
 
char java_char_from_type (const typet &type)
 
std::vector< typetjava_generic_type_from_string (const std::string &, const std::string &)
 Converts the content of a generic class type into a vector of Java types, that is each type variable of the class has one entry in the returned vector. More...
 
typet java_bytecode_promotion (const typet &)
 Java does not support byte/short return types. These are always promoted. More...
 
exprt java_bytecode_promotion (const exprt &)
 Java does not support byte/short return types. These are always promoted. More...
 
size_t find_closing_semi_colon_for_reference_type (const std::string src, size_t starting_point=0)
 Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point. More...
 
std::vector< std::string > parse_raw_list_types (std::string src, char opening_bracket, char closing_bracket)
 Given a substring of a descriptor or signature that contains one or more types parse out the individual type strings. More...
 
bool is_java_array_tag (const irep_idt &tag)
 See above. More...
 
bool is_valid_java_array (const struct_typet &)
 Programmatic documentation of the structure of a Java array (of either primitives or references) type. More...
 
bool equal_java_types (const typet &type1, const typet &type2)
 Compares the types, including checking element types if both types are arrays. More...
 
bool is_java_generic_parameter_tag (const typet &type)
 Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. More...
 
const java_generic_parameter_tagtto_java_generic_parameter_tag (const typet &type)
 
java_generic_parameter_tagtto_java_generic_parameter_tag (typet &type)
 
template<>
bool can_cast_type< java_generic_parametert > (const typet &base)
 Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T>. More...
 
bool is_java_generic_parameter (const typet &type)
 Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. More...
 
const java_generic_parametertto_java_generic_parameter (const typet &type)
 
java_generic_parametertto_java_generic_parameter (typet &type)
 
bool is_java_generic_struct_tag_type (const typet &type)
 
const java_generic_struct_tag_typetto_java_generic_struct_tag_type (const typet &type)
 
java_generic_struct_tag_typetto_java_generic_struct_tag_type (typet &type)
 
template<>
bool can_cast_type< java_generic_typet > (const typet &type)
 
bool is_java_generic_type (const typet &type)
 
const java_generic_typetto_java_generic_type (const typet &type)
 
java_generic_typetto_java_generic_type (typet &type)
 
bool is_java_generic_class_type (const typet &type)
 
const java_generic_class_typetto_java_generic_class_type (const java_class_typet &type)
 
java_generic_class_typetto_java_generic_class_type (java_class_typet &type)
 
const typetjava_generic_get_inst_type (size_t index, const java_generic_typet &type)
 Access information of type arguments of java instantiated type. More...
 
const irep_idtjava_generic_class_type_var (size_t index, const java_generic_class_typet &type)
 Access information of type variables of a generic java class type. More...
 
const typetjava_generic_class_type_bound (size_t index, const typet &t)
 Access information of the type bound of a generic java class type. More...
 
bool is_java_implicitly_generic_class_type (const typet &type)
 
const java_implicitly_generic_class_typetto_java_implicitly_generic_class_type (const java_class_typet &type)
 
java_implicitly_generic_class_typetto_java_implicitly_generic_class_type (java_class_typet &type)
 
std::vector< java_generic_parametertget_all_generic_parameters (const typet &type)
 
std::optional< typetjava_type_from_string_with_exception (const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name)
 
const std::optional< size_t > java_generics_get_index_for_subtype (const std::vector< java_generic_parametert > &gen_types, const irep_idt &identifier)
 Get the index in the subtypes array for a given component. More...
 
void get_dependencies_from_generic_parameters (const std::string &, std::set< irep_idt > &)
 Collect information about generic type parameters from a given signature. More...
 
void get_dependencies_from_generic_parameters (const typet &, std::set< irep_idt > &)
 Collect information about generic type parameters from a given type. More...
 
std::string erase_type_arguments (const std::string &)
 Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet More...
 
std::string gather_full_class_name (const std::string &)
 Returns the full class name, skipping over the generics. More...
 
std::string pretty_java_type (const typet &)
 
std::string pretty_signature (const java_method_typet &)
 

Macro Definition Documentation

◆ JAVA_ARRAY_DIMENSION_FIELD_NAME

#define JAVA_ARRAY_DIMENSION_FIELD_NAME   "@array_dimensions"

Definition at line 668 of file java_types.h.

◆ JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME

#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME   "@element_class_identifier"

Definition at line 670 of file java_types.h.

◆ JAVA_REFERENCE_ARRAY_CLASSID

#define JAVA_REFERENCE_ARRAY_CLASSID   "java::array[reference]"

Definition at line 655 of file java_types.h.

Function Documentation

◆ can_cast_type< annotated_typet >()

template<>
bool can_cast_type< annotated_typet > ( const typet )
inline

Definition at line 94 of file java_types.h.

◆ can_cast_type< java_class_typet >()

template<>
bool can_cast_type< java_class_typet > ( const typet type)
inline

Definition at line 594 of file java_types.h.

◆ can_cast_type< java_generic_parametert >()

template<>
bool can_cast_type< java_generic_parametert > ( const typet base)
inline

Check whether a reference to a typet is a Java generic parameter/variable, e.g., T in List<T>.

Parameters
baseSource type.
Returns
True if type is a generic Java parameter type

Definition at line 809 of file java_types.h.

◆ can_cast_type< java_generic_typet >()

template<>
bool can_cast_type< java_generic_typet > ( const typet type)
inline

Definition at line 938 of file java_types.h.

◆ can_cast_type< java_method_typet >()

template<>
bool can_cast_type< java_method_typet > ( const typet type)
inline

Definition at line 178 of file java_types.h.

◆ can_cast_type< java_reference_typet >()

template<>
bool can_cast_type< java_reference_typet > ( const typet type)
inline

Definition at line 623 of file java_types.h.

◆ equal_java_types()

bool equal_java_types ( const typet type1,
const typet type2 
)

Compares the types, including checking element types if both types are arrays.

Parameters
type1First type to compare
type2Second type to compare
Returns
True if the types are equal, including elemnt types if they are both arrays

Definition at line 895 of file java_types.cpp.

◆ erase_type_arguments()

std::string erase_type_arguments ( const std::string &  src)

Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet

Take a signature string and remove everything in angle brackets allowing for the type to be parsed normally, for example java.util.HashSet<java.lang.Integer> will be turned into java.util.HashSet

Parameters
srcThe input string
Returns
The input string with everything between angle brackets removed

Definition at line 334 of file java_types.cpp.

◆ find_closing_semi_colon_for_reference_type()

size_t find_closing_semi_colon_for_reference_type ( const std::string  src,
size_t  starting_point 
)

Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.

Parameters
srcThe input string to work on.
starting_pointThe string position where the opening 'L' we want to find the closing ';' for.
Returns
The string position corresponding to the matching ';'. For example: LA;, we would return 2. For LA<TT;>; we would return 7. See unit/java_bytecode/java_util_tests.cpp for more examples.

Definition at line 516 of file java_types.cpp.

◆ gather_full_class_name()

std::string gather_full_class_name ( const std::string &  src)

Returns the full class name, skipping over the generics.

This turns any of these:

  1. Signature: Lcom/package/OuterClass<TT;>.Inner;
  2. Descriptor: Lcom.pacakge.OuterClass$Inner; into com.package.OuterClass.Inner
Parameters
srca type descriptor or signature
  1. Signature: Lcom/package/OuterClass<TT;>.Inner;
  2. Descriptor: Lcom.package.OuterClass$Inner;
Returns
The full name of the class like com.package.OuterClass.Inner (for both examples).

Definition at line 365 of file java_types.cpp.

◆ get_all_generic_parameters()

std::vector<java_generic_parametert> get_all_generic_parameters ( const typet type)
Parameters
typeSource type
Returns
The vector of implicitly generic and (explicitly) generic type parameters of the given type.

Definition at line 924 of file java_types.cpp.

◆ get_array_dimension_field()

exprt get_array_dimension_field ( const exprt pointer)
Parameters
pointerpointer to an array[reference] object
Returns
member expression to access its array dimension field

Definition at line 206 of file java_types.cpp.

◆ get_array_element_type_field()

exprt get_array_element_type_field ( const exprt pointer)
Parameters
pointerpointer to an array[reference] object
Returns
member expression to access its array element_type field

Definition at line 218 of file java_types.cpp.

◆ get_dependencies_from_generic_parameters() [1/2]

void get_dependencies_from_generic_parameters ( const std::string &  signature,
std::set< irep_idt > &  refs 
)

Collect information about generic type parameters from a given signature.

This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.

Parameters
signaturethe string representation of the signature to analyze
[out]refsthe set to insert the names of the found dependencies

Definition at line 996 of file java_types.cpp.

◆ get_dependencies_from_generic_parameters() [2/2]

void get_dependencies_from_generic_parameters ( const typet t,
std::set< irep_idt > &  refs 
)

Collect information about generic type parameters from a given type.

This is used to get information about class dependencies that must be loaded but only appear as generic type argument, not as a field reference.

Parameters
tthe type to analyze
[out]refsthe set to insert the names of the found dependencies

Definition at line 1032 of file java_types.cpp.

◆ is_java_array_tag()

bool is_java_array_tag ( const irep_idt tag)

See above.

Parameters
tagTag of a struct
Returns
True if the given string is a Java array tag, i.e., has a prefix of java::array[

Definition at line 233 of file java_types.cpp.

◆ is_java_array_type()

bool is_java_array_type ( const typet type)

Checks whether the given type is an array pointer type.

Definition at line 163 of file java_types.cpp.

◆ is_java_generic_class_type()

bool is_java_generic_class_type ( const typet type)
inline
Parameters
typethe type to check
Returns
true if type is a java class type with generics

Definition at line 994 of file java_types.h.

◆ is_java_generic_parameter()

bool is_java_generic_parameter ( const typet type)
inline

Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.

Parameters
typethe type to check
Returns
true if type is a generic Java parameter type

Definition at line 819 of file java_types.h.

◆ is_java_generic_parameter_tag()

bool is_java_generic_parameter_tag ( const typet type)
inline

Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.

Parameters
typethe type to check
Returns
true if type is a generic Java parameter tag type

Definition at line 750 of file java_types.h.

◆ is_java_generic_struct_tag_type()

bool is_java_generic_struct_tag_type ( const typet type)
inline
Parameters
typethe type to check
Returns
true if the type is a symbol type with generics

Definition at line 888 of file java_types.h.

◆ is_java_generic_type()

bool is_java_generic_type ( const typet type)
inline
Parameters
typethe type to check
Returns
true if type is java type containing with generics, e.g., List<T>

Definition at line 946 of file java_types.h.

◆ is_java_implicitly_generic_class_type()

bool is_java_implicitly_generic_class_type ( const typet type)
inline
Parameters
typethe type to check
Returns
true if type is a implicitly generic java class type

Definition at line 1099 of file java_types.h.

◆ is_multidim_java_array_type()

bool is_multidim_java_array_type ( const typet type)

Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array type with element type also being a pointer to an array type.

Definition at line 179 of file java_types.cpp.

◆ is_valid_java_array()

bool is_valid_java_array ( const struct_typet type)

Programmatic documentation of the structure of a Java array (of either primitives or references) type.

A Java array is represented in GOTO in the following way: A struct component with a tag like java::array[type] where type is either a primitive like int, or reference. The struct has precisely three components:

  1. @java.lang.Object: of type struct {java.lang.Object} containing the base class data
  2. length: of type Java integer - the length of the array
  3. data: of type pointer to either pointer to a primitive type, or pointer to pointer to empty (i.e. a void**) pointing to the contents of the array
    Parameters
    typeA type that might represent a Java array
    Returns
    True if it is a Java array type, false otherwise

Definition at line 838 of file java_types.cpp.

◆ java_array_dimension_and_element_type()

std::pair<typet, std::size_t> java_array_dimension_and_element_type ( const struct_tag_typet type)

Returns the underlying element type and array dimensionality of Java struct type.

If this is not an array type the return value will be {type, 0}.

Definition at line 189 of file java_types.cpp.

◆ java_array_element_type() [1/2]

const typet& java_array_element_type ( const struct_tag_typet array_symbol)

Return a const reference to the element type of a given java array type.

Parameters
array_symbolThe java array type

Definition at line 144 of file java_types.cpp.

◆ java_array_element_type() [2/2]

typet& java_array_element_type ( struct_tag_typet array_symbol)

Return a non-const reference to the element type of a given java array type.

Parameters
array_symbolThe java array type

Definition at line 154 of file java_types.cpp.

◆ java_array_type()

java_reference_typet java_array_type ( const char  subtype)

Construct an array pointer type.

It is a pointer to a symbol with identifier java::array[]. Its ID_element_type is set to the corresponding primitive type, or void* for arrays of references.

Parameters
subtypeCharacter indicating the type of array

Definition at line 109 of file java_types.cpp.

◆ java_boolean_type()

c_bool_typet java_boolean_type ( )

Definition at line 79 of file java_types.cpp.

◆ java_byte_type()

signedbv_typet java_byte_type ( )

Definition at line 55 of file java_types.cpp.

◆ java_bytecode_promotion() [1/2]

exprt java_bytecode_promotion ( const exprt expr)

Java does not support byte/short return types. These are always promoted.

Definition at line 281 of file java_types.cpp.

◆ java_bytecode_promotion() [2/2]

typet java_bytecode_promotion ( const typet type)

Java does not support byte/short return types. These are always promoted.

Definition at line 269 of file java_types.cpp.

◆ java_char_from_type()

char java_char_from_type ( const typet type)

Definition at line 708 of file java_types.cpp.

◆ java_char_type()

unsignedbv_typet java_char_type ( )

Definition at line 61 of file java_types.cpp.

◆ java_classname()

struct_tag_typet java_classname ( const std::string &  id)

Definition at line 809 of file java_types.cpp.

◆ java_double_type()

floatbv_typet java_double_type ( )

Definition at line 73 of file java_types.cpp.

◆ java_float_type()

floatbv_typet java_float_type ( )

Definition at line 67 of file java_types.cpp.

◆ java_generic_class_type_bound()

const typet& java_generic_class_type_bound ( size_t  index,
const typet t 
)
inline

Access information of the type bound of a generic java class type.

Parameters
indexthe index of the type variable
tthe type from which to extract the type bound
Returns
the type of the bound of the type variable

Definition at line 1050 of file java_types.h.

◆ java_generic_class_type_var()

const irep_idt& java_generic_class_type_var ( size_t  index,
const java_generic_class_typet type 
)
inline

Access information of type variables of a generic java class type.

Parameters
indexthe index of the type variable
typethe type from which to extract the type variable
Returns
the name of the generic type variable of t at the given index

Definition at line 1036 of file java_types.h.

◆ java_generic_get_inst_type()

const typet& java_generic_get_inst_type ( size_t  index,
const java_generic_typet type 
)
inline

Access information of type arguments of java instantiated type.

Parameters
indexthe index of the type argument
typethe type from which to extract the type argument
Returns
the type variable of t at the given index

Definition at line 1021 of file java_types.h.

◆ java_generic_type_from_string()

std::vector<typet> java_generic_type_from_string ( const std::string &  class_name,
const std::string &  src 
)

Converts the content of a generic class type into a vector of Java types, that is each type variable of the class has one entry in the returned vector.

This also supports parsing of bounds in the form of <T:CBound> for classes or <T::IBound> for interfaces.

For example for HashMap<K, V> a vector with two elements would be returned

Returns
vector of java types representing the generic type variables

the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;> or of the form <TX::Bound_X;:BoundZ;TY:Bound_Y;> if Bound_X is an interface

Definition at line 749 of file java_types.cpp.

◆ java_generics_get_index_for_subtype()

const std::optional<size_t> java_generics_get_index_for_subtype ( const std::vector< java_generic_parametert > &  gen_types,
const irep_idt identifier 
)
inline

Get the index in the subtypes array for a given component.

Parameters
gen_typesThe subtypes array.
identifierThe string identifier of the type of the component.
Returns
Optional with the size if the identifier was found.

Definition at line 1159 of file java_types.h.

◆ java_int_type()

signedbv_typet java_int_type ( )

Definition at line 31 of file java_types.cpp.

◆ java_lang_object_type()

java_reference_typet java_lang_object_type ( )

Definition at line 98 of file java_types.cpp.

◆ java_long_type()

signedbv_typet java_long_type ( )

Definition at line 43 of file java_types.cpp.

◆ java_reference_array_type()

java_reference_typet java_reference_array_type ( const struct_tag_typet element_type)

Definition at line 541 of file java_types.cpp.

◆ java_reference_type() [1/2]

java_reference_typet java_reference_type ( const struct_tag_typet subtype)

Definition at line 93 of file java_types.cpp.

◆ java_reference_type() [2/2]

reference_typet java_reference_type ( const typet subtype)

Definition at line 88 of file java_types.cpp.

◆ java_short_type()

signedbv_typet java_short_type ( )

Definition at line 49 of file java_types.cpp.

◆ java_type_from_char()

typet java_type_from_char ( char  t)

Constructs a type indicated by the given character:

  • i integer
  • l long
  • s short
  • b byte
  • c character
  • f float
  • d double
  • z boolean
  • a reference

Definition at line 248 of file java_types.cpp.

◆ java_type_from_string()

std::optional<typet> java_type_from_string ( const std::string &  src,
const std::string &  class_name_prefix 
)

Transforms a string representation of a Java type into an internal type representation thereof.

Example use are object types like "Ljava/lang/Integer;", type variables/parameters like "TE;" which require a non-empty class_name_prefix or generic types like "Ljava/util/List<TE;>;" or "Ljava/util/List<Ljava/lang/Integer;>;" also requiring class_name_prefix.

Parameters
srcthe string representation as used in the class file
class_name_prefixname of class to append to generic type variables/parameters
Returns
internal type representation for GOTO programs

Definition at line 561 of file java_types.cpp.

◆ java_type_from_string_with_exception()

std::optional<typet> java_type_from_string_with_exception ( const std::string &  descriptor,
const std::optional< std::string > &  signature,
const std::string &  class_name 
)
inline

Definition at line 1140 of file java_types.h.

◆ java_void_type()

empty_typet java_void_type ( )

Definition at line 37 of file java_types.cpp.

◆ parse_raw_list_types()

std::vector<std::string> parse_raw_list_types ( const std::string  src,
const char  opening_bracket,
const char  closing_bracket 
)

Given a substring of a descriptor or signature that contains one or more types parse out the individual type strings.

Parameters
srcThe input string that is wrapped in either ( ) or < >
opening_bracketFor checking string is passed in as expected, the opening bracket (i.e. '(' or '<').
closing_bracketFor checking string is passed in as expected, the closing bracket (i.e. ')' or '>').
Returns
A vector of strings that represent the bytecode type.

Definition at line 419 of file java_types.cpp.

◆ pretty_java_type()

std::string pretty_java_type ( const typet type)

Definition at line 1089 of file java_types.cpp.

◆ pretty_signature()

std::string pretty_signature ( const java_method_typet method_type)

Definition at line 1131 of file java_types.cpp.

◆ to_annotated_type() [1/2]

const annotated_typet& to_annotated_type ( const typet type)
inline

Definition at line 83 of file java_types.h.

◆ to_annotated_type() [2/2]

annotated_typet& to_annotated_type ( typet type)
inline

Definition at line 88 of file java_types.h.

◆ to_java_class_type() [1/2]

const java_class_typet& to_java_class_type ( const typet type)
inline

Definition at line 581 of file java_types.h.

◆ to_java_class_type() [2/2]

java_class_typet& to_java_class_type ( typet type)
inline

Definition at line 587 of file java_types.h.

◆ to_java_generic_class_type() [1/2]

const java_generic_class_typet& to_java_generic_class_type ( const java_class_typet type)
inline
Parameters
typethe type to check
Returns
cast of type to java_generics_class_typet

Definition at line 1002 of file java_types.h.

◆ to_java_generic_class_type() [2/2]

java_generic_class_typet& to_java_generic_class_type ( java_class_typet type)
inline
Parameters
typesource type
Returns
cast of type into a java class type with generics

Definition at line 1011 of file java_types.h.

◆ to_java_generic_parameter() [1/2]

const java_generic_parametert& to_java_generic_parameter ( const typet type)
inline
Parameters
typesource type
Returns
cast of type into a java_generic_parametert

Definition at line 826 of file java_types.h.

◆ to_java_generic_parameter() [2/2]

java_generic_parametert& to_java_generic_parameter ( typet type)
inline
Parameters
typesource type
Returns
cast of type into a java_generic_parameter

Definition at line 835 of file java_types.h.

◆ to_java_generic_parameter_tag() [1/2]

const java_generic_parameter_tagt& to_java_generic_parameter_tag ( const typet type)
inline
Parameters
typesource type
Returns
cast of type into a java_generic_parametert

Definition at line 758 of file java_types.h.

◆ to_java_generic_parameter_tag() [2/2]

java_generic_parameter_tagt& to_java_generic_parameter_tag ( typet type)
inline
Parameters
typesource type
Returns
cast of type into a java_generic_parameter_tag

Definition at line 766 of file java_types.h.

◆ to_java_generic_struct_tag_type() [1/2]

const java_generic_struct_tag_typet& to_java_generic_struct_tag_type ( const typet type)
inline
Parameters
typethe type to convert
Returns
the converted type

Definition at line 896 of file java_types.h.

◆ to_java_generic_struct_tag_type() [2/2]

java_generic_struct_tag_typet& to_java_generic_struct_tag_type ( typet type)
inline
Parameters
typethe type to convert
Returns
the converted type

Definition at line 905 of file java_types.h.

◆ to_java_generic_type() [1/2]

const java_generic_typet& to_java_generic_type ( const typet type)
inline
Parameters
typesource type
Returns
cast of type into java type with generics

Definition at line 953 of file java_types.h.

◆ to_java_generic_type() [2/2]

java_generic_typet& to_java_generic_type ( typet type)
inline
Parameters
typesource type
Returns
cast of type into java type with generics

Definition at line 962 of file java_types.h.

◆ to_java_implicitly_generic_class_type() [1/2]

const java_implicitly_generic_class_typet& to_java_implicitly_generic_class_type ( const java_class_typet type)
inline
Parameters
typethe type to check
Returns
cast of type to java_generics_class_typet

Definition at line 1107 of file java_types.h.

◆ to_java_implicitly_generic_class_type() [2/2]

java_implicitly_generic_class_typet& to_java_implicitly_generic_class_type ( java_class_typet type)
inline
Parameters
typesource type
Returns
cast of type into a java class type with generics

Definition at line 1116 of file java_types.h.

◆ to_java_method_type() [1/2]

const java_method_typet& to_java_method_type ( const typet type)
inline

Definition at line 183 of file java_types.h.

◆ to_java_method_type() [2/2]

java_method_typet& to_java_method_type ( typet type)
inline

Definition at line 189 of file java_types.h.

◆ to_java_reference_type() [1/2]

const java_reference_typet& to_java_reference_type ( const typet type)
inline

Definition at line 629 of file java_types.h.

◆ to_java_reference_type() [2/2]

java_reference_typet& to_java_reference_type ( typet type)
inline

Definition at line 635 of file java_types.h.