cprover
Loading...
Searching...
No Matches
require_type.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: 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)
23namespace require_type
24{
26require_pointer(const typet &type, const optionalt<typet> &subtype);
27
28const struct_tag_typet &
29require_struct_tag(const typet &type, const irep_idt &identifier = "");
30
32 const typet &type,
33 const irep_idt &identifier = irep_idt());
34
36 const java_class_typet &java_class_type,
37 const irep_idt &component_name);
38
40 const struct_typet &struct_type,
41 const irep_idt &component_name);
42
43code_typet require_code(const typet &type);
45
47require_parameter(const code_typet &function_type, const irep_idt &param_name);
48
49code_typet require_code(const typet &type, const size_t num_params);
51require_java_method(const typet &type, const size_t num_params);
52
53// A mini DSL for describing an expected set of type arguments for a
54// java_generic_typet
56{
57 Inst,
58 Var
59};
61{
64};
65typedef std::initializer_list<expected_type_argumentt>
67
69
71 const typet &type,
72 const require_type::expected_type_argumentst &type_expectations);
73
75
77 const typet &type,
78 const irep_idt &parameter);
79
81 const typet &type,
82 const optionalt<struct_tag_typet> &expect_subtype);
83
85
87
89
91 const typet &class_type,
92 const std::initializer_list<irep_idt> &type_variables);
93
96
98 const typet &class_type,
99 const std::initializer_list<irep_idt> &type_parameters);
100
103
105 const typet &class_type,
106 const std::initializer_list<irep_idt> &implicit_type_variables);
107
110
113 const typet &class_type,
114 const std::initializer_list<irep_idt> &implicit_type_variables);
115
117
120
122 const typet &type,
123 const std::string &identifier);
124
126 const typet &type,
127 const std::string &identifier,
128 const require_type::expected_type_argumentst &type_expectations);
129
132
134 const java_class_typet &class_type,
135 const std::vector<std::string> &expected_identifiers);
136}
137
138#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
Class type.
Definition std_types.h:325
Base type of functions.
Definition std_types.h:539
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition java_types.h:515
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition java_types.h:973
Reference that points to a java_generic_parameter_tagt.
Definition java_types.h:776
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition java_types.h:858
Reference that points to a java_generic_struct_tag_typet.
Definition java_types.h:915
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
Structure type, corresponds to C style structs.
Definition std_types.h:231
The type of an expression, extends irept.
Definition type.h:29
dstringt irep_idt
Definition irep.h:37
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.
class_typet require_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
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.
pointer_typet require_pointer_to_tag(const typet &type, const irep_idt &identifier=irep_idt())
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.
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.
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
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.
std::initializer_list< expected_type_argumentt > expected_type_argumentst
class_typet require_complete_class(const typet &class_type)
Checks that the given type is a complete class.
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid 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.
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.
java_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
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.
java_method_typet require_java_method(const typet &type)
Checks a type is a java_method_typet (i.e.
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.
nonstd::optional< T > optionalt
Definition optional.h:35
Pre-defined types.