File tree 2 files changed +35
-0
lines changed
2 files changed +35
-0
lines changed Original file line number Diff line number Diff line change @@ -480,3 +480,31 @@ java_generic_symbol_typet require_type::require_java_generic_symbol_type(
480
480
481
481
return generic_base_type;
482
482
}
483
+
484
+ // / Verify that the lambda method handles of a class match the given
485
+ // / expectation.
486
+ // / \param class_struct class type to be verified
487
+ // / \param expected_identifiers expected list of lambda method handle
488
+ // / references
489
+ // / \return lambda method handles of the class
490
+ require_type::java_lambda_method_handlest
491
+ require_type::require_lambda_method_handles (
492
+ const java_class_typet &class_type,
493
+ const std::vector<std::string> &expected_identifiers)
494
+ {
495
+ const require_type::java_lambda_method_handlest &lambda_method_handles =
496
+ class_type.lambda_method_handles ();
497
+ REQUIRE (lambda_method_handles.size () == expected_identifiers.size ());
498
+
499
+ REQUIRE (
500
+ std::equal (
501
+ lambda_method_handles.begin (),
502
+ lambda_method_handles.end (),
503
+ expected_identifiers.begin (),
504
+ [](
505
+ const symbol_exprt &lambda_method_handle,
506
+ const std::string &expected_identifier) { // NOLINT
507
+ return lambda_method_handle.get_identifier () == expected_identifier;
508
+ }));
509
+ return lambda_method_handles;
510
+ }
Original file line number Diff line number Diff line change @@ -115,6 +115,13 @@ java_generic_symbol_typet require_java_generic_symbol_type(
115
115
const typet &type,
116
116
const std::string &identifier,
117
117
const require_type::expected_type_argumentst &type_expectations);
118
+
119
+ typedef java_class_typet::java_lambda_method_handlest
120
+ java_lambda_method_handlest;
121
+
122
+ java_lambda_method_handlest require_lambda_method_handles (
123
+ const java_class_typet &class_type,
124
+ const std::vector<std::string> &expected_identifiers);
118
125
}
119
126
120
127
#endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H
You can’t perform that action at this time.
0 commit comments