cprover
require_type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Unit test utilities
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
14 
15 #ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
16 #define CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
17 
18 #include <util/optional.h>
19 #include <util/std_types.h>
21 
22 // NOLINTNEXTLINE(readability/namespace)
23 namespace require_type
24 {
26 require_pointer(const typet &type, const optionalt<typet> &subtype);
27 
28 const struct_tag_typet &
29 require_struct_tag(const typet &type, const irep_idt &identifier = "");
30 
32  const struct_typet &struct_type,
33  const irep_idt &component_name);
34 
35 code_typet require_code(const typet &type);
37 
39 require_parameter(const code_typet &function_type, const irep_idt &param_name);
40 
41 code_typet require_code(const typet &type, const size_t num_params);
43 require_java_method(const typet &type, const size_t num_params);
44 
45 // A mini DSL for describing an expected set of type arguments for a
46 // java_generic_typet
48 {
49  Inst,
50  Var
51 };
53 {
56 };
57 typedef std::initializer_list<expected_type_argumentt>
59 
61 
63  const typet &type,
64  const require_type::expected_type_argumentst &type_expectations);
65 
67 
69  const typet &type,
70  const irep_idt &parameter);
71 
73  const typet &type,
74  const optionalt<struct_tag_typet> &expect_subtype);
75 
76 class_typet require_complete_class(const typet &class_type);
77 
78 class_typet require_incomplete_class(const typet &class_type);
79 
81 
83  const typet &class_type,
84  const std::initializer_list<irep_idt> &type_variables);
85 
88 
90  const typet &class_type,
91  const std::initializer_list<irep_idt> &type_parameters);
92 
95 
97  const typet &class_type,
98  const std::initializer_list<irep_idt> &implicit_type_variables);
99 
102 
105  const typet &class_type,
106  const std::initializer_list<irep_idt> &implicit_type_variables);
107 
109 
112 
114  const typet &type,
115  const std::string &identifier);
116 
118  const typet &type,
119  const std::string &identifier,
120  const require_type::expected_type_argumentst &type_expectations);
121 
124 
126  const java_class_typet &class_type,
127  const std::vector<std::string> &expected_identifiers);
128 }
129 
130 #endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
require_type::require_code
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
Definition: require_type.cpp:58
require_type::expected_type_argumentt::description
irep_idt description
Definition: require_type.h:55
class_typet
Class type.
Definition: std_types.h:365
java_generic_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:483
require_type::require_java_generic_struct_tag_type
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.
Definition: require_type.cpp:467
typet
The type of an expression, extends irept.
Definition: type.h:27
require_type::expected_type_argumentst
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:58
require_type::require_complete_java_implicitly_generic_class
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.
Definition: require_type.cpp:396
optional.h
require_type::java_lambda_method_handlest
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:123
java_generic_parametert
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
require_type::expected_type_argumentt
Definition: require_type.h:52
require_type::require_java_non_generic_type
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.
Definition: require_type.cpp:228
java_class_typet
Definition: java_types.h:101
require_type::require_java_generic_type
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
Definition: require_type.cpp:155
require_type::require_java_implicitly_generic_class
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.
Definition: require_type.cpp:343
require_type::require_lambda_method_handles
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.
Definition: require_type.cpp:518
require_type::require_complete_class
class_typet require_complete_class(const typet &class_type)
Checks that the given type is a complete class.
Definition: require_type.cpp:242
require_type::type_argument_kindt::Var
require_type::require_java_generic_parameter
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
Definition: require_type.cpp:197
require_type::require_java_method
java_method_typet require_java_method(const typet &type)
Checks a type is a java_method_typet (i.e.
Definition: require_type.cpp:81
std_types.h
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 o...
Definition: java_types.h:637
require_type::require_complete_java_non_generic_class
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
Definition: require_type.cpp:440
require_type::type_argument_kindt::Inst
code_typet
Base type of functions.
Definition: std_types.h:751
require_type::require_java_generic_class
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid java generic class.
Definition: require_type.cpp:271
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
require_type
Definition: require_type.h:23
java_class_typet::java_lambda_method_handlest
irept::subt java_lambda_method_handlest
Definition: java_types.h:196
require_type::type_argument_kindt
type_argument_kindt
Definition: require_type.h:47
struct_union_typet::componentt
Definition: std_types.h:121
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
require_type::require_incomplete_class
class_typet require_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
Definition: require_type.cpp:256
require_type::require_parameter
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.
Definition: require_type.cpp:106
require_type::require_java_non_generic_class
java_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
Definition: require_type.cpp:422
require_type::require_component
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.
Definition: require_type.cpp:40
require_type::expected_type_argumentt::kind
type_argument_kindt kind
Definition: require_type.h:54
code_typet::parametert
Definition: std_types.h:788
java_generic_struct_tag_typet
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types.
Definition: java_types.h:754
require_type::require_pointer
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
Definition: require_type.cpp:21
java_generic_class_typet
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:542
java_types.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
require_type::require_struct_tag
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.
Definition: require_type.cpp:451
java_method_typet
Definition: java_types.h:264
require_type::require_complete_java_generic_class
java_generic_class_typet require_complete_java_generic_class(const typet &class_type)
Verify that a class is a complete, valid java generic class.
Definition: require_type.cpp:320