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 symbol_typet &
29 require_symbol(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);
36 
38 require_parameter(const code_typet &function_type, const irep_idt &param_name);
39 
40 code_typet require_code(const typet &type, const size_t num_params);
41 
42 // A mini DSL for describing an expected set of type arguments for a
43 // java_generic_typet
45 {
46  Inst,
47  Var
48 };
50 {
53 };
54 typedef std::initializer_list<expected_type_argumentt>
56 
58 
60  const typet &type,
61  const require_type::expected_type_argumentst &type_expectations);
62 
64 
66  const typet &type,
67  const irep_idt &parameter);
68 
70  const typet &type,
71  const optionalt<symbol_typet> &expect_subtype);
72 
73 class_typet require_complete_class(const typet &class_type);
74 
75 class_typet require_incomplete_class(const typet &class_type);
76 
78 
80  const typet &class_type,
81  const std::initializer_list<irep_idt> &type_variables);
82 
85 
87  const typet &class_type,
88  const std::initializer_list<irep_idt> &type_parameters);
89 
92 
94  const typet &class_type,
95  const std::initializer_list<irep_idt> &implicit_type_variables);
96 
99 
102  const typet &class_type,
103  const std::initializer_list<irep_idt> &implicit_type_variables);
104 
106 
109 
111  const typet &type,
112  const std::string &identifier);
113 
115  const typet &type,
116  const std::string &identifier,
117  const require_type::expected_type_argumentst &type_expectations);
118 
121 
123  const java_class_typet &class_type,
124  const std::vector<std::string> &expected_identifiers);
125 }
126 
127 #endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
The type of an expression.
Definition: type.h:22
java_generic_class_typet require_complete_java_generic_class(const typet &class_type)
Verify that a class is a complete, valid java generic class.
Base type of functions.
Definition: std_types.h:764
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:124
java_generic_symbol_typet require_java_generic_symbol_type(const typet &type, const std::string &identifier)
Verify a given type is a java generic symbol type.
const typet & require_java_non_generic_type(const typet &type, const optionalt< symbol_typet > &expect_subtype)
Test a type to ensure it is not a java generics type.
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.
Structure type.
Definition: std_types.h:297
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.
std::initializer_list< expected_type_argumentt > expected_type_argumentst
Definition: require_type.h:55
java_class_typet::java_lambda_method_handlest java_lambda_method_handlest
Definition: require_type.h:120
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:375
A reference into the symbol table.
Definition: std_types.h:110
java_generic_parametert require_java_generic_parameter(const typet &type)
Verify a given type is a java_generic_parameter, e.g., T
The pointer type.
Definition: std_types.h:1426
nonstd::optional< T > optionalt
Definition: optional.h:35
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_complete_class(const typet &class_type)
Checks that the given type is a complete class.
const symbol_typet & require_symbol(const typet &type, const irep_idt &identifier="")
Verify a given type is a symbol type, optionally with a specific identifier.
java_generic_typet require_java_generic_type(const typet &type)
Verify a given type is a java_generic_type.
java_class_typet require_complete_java_non_generic_class(const typet &class_type)
Verify that a class is a complete, valid nongeneric java class.
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
Definition: java_types.h:587
java_generic_class_typet require_java_generic_class(const typet &class_type)
Verify that a class is a valid java generic class.
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_class_typet require_java_non_generic_class(const typet &class_type)
Verify that a class is a valid nongeneric java class.
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:318
API to type classes.
pointer_typet require_pointer(const typet &type, const optionalt< typet > &subtype)
Checks a type is a pointer type optionally with a specific subtype.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:232
code_typet require_code(const typet &type)
Checks a type is a code_type (i.e.
class_typet require_incomplete_class(const typet &class_type)
Checks that the given type is an incomplete class.
C++ class type.
Definition: std_types.h:341
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.
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:470