cprover
|
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...
#include <java_types.h>
Public Types | |
typedef std::vector< reference_typet > | generic_typest |
![]() | |
using | baset = tree_implementationt |
![]() | |
using | dt |
using | subt |
using | named_subt |
using | tree_implementationt |
Used to refer to this class from derived classes. | |
Additional Inherited Members | |
![]() | |
static void | check (const typet &, const validation_modet=validation_modet::INVARIANT) |
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked) | |
static void | validate (const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
Check that the type is well-formed, assuming that its subtypes have already been checked for well-formedness. | |
static void | validate_full (const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT) |
Check that the type is well-formed (full check, including checks of subtypes) | |
![]() | |
static bool | is_comment (const irep_idt &name) |
static std::size_t | number_of_non_comments (const named_subt &) |
count the number of named_sub elements that are not comments | |
![]() | |
void | detach () |
![]() | |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
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).
The vector holds the types of the type arguments (all of type or subtype of reference_typet), that is the vector has the length of the number of type parameters of the generic class. For example:
HashMap<K, V>
it would contain two elements, each of type java_generic_parametert
,HashMap<Integer, V>
it would contain two elements, the first of type reference_typet
and the second of type java_generic_parametert
,HashMap<List<T>, V>
it would contain two elements, the first of type java_generic_typet
and the second of type java_generic_parametert
. Definition at line 857 of file java_types.h.
Definition at line 860 of file java_types.h.
|
inlineexplicit |
Definition at line 862 of file java_types.h.
java_generic_struct_tag_typet::java_generic_struct_tag_typet | ( | const struct_tag_typet & | type, |
const std::string & | base_ref, | ||
const std::string & | class_name_prefix ) |
Construct a generic symbol type by extending the symbol type type
with generic types extracted from the reference base_ref
.
This assumes that the class named class_name_prefix
extends or implements the class type
, and that base_ref
corresponds to a generic class. For instance since HashMap<K,V> extends Map<K,V> we would call java_generic_struct_tag_typet(struct_tag_typet("Map"), "Ljava/util/Map<TK;TV;>;", "java.util.HashMap")
which generates a symbol type with identifier "Map", and two generic types with identifier "java.util.HashMap::K" and "java.util.HashMap::V" respectively.
Definition at line 1048 of file java_types.cpp.
optionalt< size_t > java_generic_struct_tag_typet::generic_type_index | ( | const java_generic_parametert & | type | ) | const |
Check if this symbol has the given generic type.
If yes, return its index in the vector of generic types.
type | The parameter type we are looking for. |
Definition at line 1075 of file java_types.cpp.
|
inline |
Definition at line 878 of file java_types.h.
|
inline |
Definition at line 873 of file java_types.h.