Skip to content

Commit 6b4cb9e

Browse files
jeannielynnmoultonjeannielynnmoulton
committed
Reinstate require_code and add require_java_method
1 parent c98e76a commit 6b4cb9e

File tree

9 files changed

+117
-85
lines changed

9 files changed

+117
-85
lines changed

‎jbmc/unit/java-testing-utils/require_type.cpp‎

Lines changed: 28 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -54,10 +54,33 @@ struct_union_typet::componentt require_type::require_component(
5454

5555
/// Checks a type is a code_type (i.e. a function)
5656
/// \param type: The type to check
57-
/// \return The cast version of the type method_type
58-
java_method_typet require_type::require_code(const typet &type)
57+
/// \return The cast version of the type code_type
58+
code_typet require_type::require_code(const typet &type)
5959
{
6060
REQUIRE(type.id() == ID_code);
61+
return to_code_type(type);
62+
}
63+
64+
/// Verify a given type is an code_typet, and that the code it represents
65+
/// accepts a given number of parameters
66+
/// \param type The type to check
67+
/// \param num_params check the the given code_typet expects this
68+
/// number of parameters
69+
/// \return The type cast to a code_typet
70+
code_typet
71+
require_type::require_code(const typet &type, const size_t num_params)
72+
{
73+
code_typet code_type = require_code(type);
74+
REQUIRE(code_type.parameters().size() == num_params);
75+
return code_type;
76+
}
77+
78+
/// Checks a type is a java_method_typet (i.e. a function)
79+
/// \param type: The type to check
80+
/// \return The cast version of the type method_type
81+
java_method_typet require_type::require_java_method(const typet &type)
82+
{
83+
REQUIRE(can_cast_type<java_method_typet>(type));
6184
return to_java_method_type(type);
6285
}
6386

@@ -68,9 +91,9 @@ java_method_typet require_type::require_code(const typet &type)
6891
/// number of parameters
6992
/// \return The type cast to a java_method_typet
7093
java_method_typet
71-
require_type::require_code(const typet &type, const size_t num_params)
94+
require_type::require_java_method(const typet &type, const size_t num_params)
7295
{
73-
java_method_typet method_type = require_code(type);
96+
java_method_typet method_type = require_java_method(type);
7497
REQUIRE(method_type.parameters().size() == num_params);
7598
return method_type;
7699
}
@@ -80,7 +103,7 @@ require_type::require_code(const typet &type, const size_t num_params)
80103
/// \param param_name: The name of the parameter
81104
/// \return: A reference to the parameter structure corresponding to this
82105
/// parameter name.
83-
java_method_typet::parametert require_type::require_parameter(
106+
code_typet::parametert require_type::require_parameter(
84107
const java_method_typet &function_type,
85108
const irep_idt &param_name)
86109
{

‎jbmc/unit/java-testing-utils/require_type.h‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,12 +32,15 @@ struct_typet::componentt require_component(
3232
const struct_typet &struct_type,
3333
const irep_idt &component_name);
3434

35-
java_method_typet require_code(const typet &type);
35+
code_typet require_code(const typet &type);
36+
java_method_typet require_java_method(const typet &type);
3637

3738
java_method_typet::parametert
3839
require_parameter(const java_method_typet &function_type, const irep_idt &param_name);
3940

40-
java_method_typet require_code(const typet &type, const size_t num_params);
41+
code_typet require_code(const typet &type, const size_t num_params);
42+
java_method_typet
43+
require_java_method(const typet &type, const size_t num_params);
4144

4245
// A mini DSL for describing an expected set of type arguments for a
4346
// java_generic_typet

‎jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ void require_is_constructor(const test_datat &test_data)
3333
test_data.symbol_table.lookup_ref(test_data.constructor_descriptor);
3434
THEN("The constructor should be marked as a constructor")
3535
{
36-
java_method_typet constructor_type = require_type::require_code(constructor.type);
36+
java_method_typet constructor_type =
37+
require_type::require_java_method(constructor.type);
3738
REQUIRE(constructor_type.get_is_constructor());
3839
}
3940
}
@@ -49,7 +50,8 @@ void require_is_static_initializer(const test_datat &test_data)
4950
test_data.symbol_table.lookup_ref(test_data.constructor_descriptor);
5051
THEN("The constructor should be marked as a constructor")
5152
{
52-
java_method_typet constructor_type = require_type::require_code(constructor.type);
53+
java_method_typet constructor_type =
54+
require_type::require_java_method(constructor.type);
5355
REQUIRE_FALSE(constructor_type.get_is_constructor());
5456
}
5557
}

‎jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ SCENARIO(
4444
symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I");
4545

4646
const java_method_typet &function_type =
47-
require_type::require_code(function_symbol.type);
47+
require_type::require_java_method(function_symbol.type);
4848
THEN("The method should be marked as a bridge method")
4949
{
5050
REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method));

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ SCENARIO(
7777
const symbolt &method_symbol =
7878
new_symbol_table.lookup_ref(method_name);
7979
const java_method_typet &method_type =
80-
require_type::require_code(method_symbol.type);
80+
require_type::require_java_method(method_symbol.type);
8181
const java_method_typet::parametert &param =
8282
require_type::require_parameter(method_type, "x");
8383
require_type::require_java_generic_parameter(

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ SCENARIO(
3333
const symbolt func_symbol =
3434
new_symbol_table.lookup_ref(process_func_name);
3535
const java_method_typet &func_code =
36-
require_type::require_code(func_symbol.type);
36+
require_type::require_java_method(func_symbol.type);
3737

3838
THEN("It has parameter x pointing to Generic")
3939
{
@@ -81,7 +81,8 @@ SCENARIO(
8181

8282
const symbolt func_symbol =
8383
new_symbol_table.lookup_ref(process_func_name);
84-
const java_method_typet func_code = require_type::require_code(func_symbol.type);
84+
const java_method_typet func_code =
85+
require_type::require_java_method(func_symbol.type);
8586

8687
THEN("It has parameter s pointing to Generic")
8788
{
@@ -129,7 +130,8 @@ SCENARIO(
129130

130131
const symbolt func_symbol =
131132
new_symbol_table.lookup_ref(process_func_name);
132-
const java_method_typet func_code = require_type::require_code(func_symbol.type);
133+
const java_method_typet func_code =
134+
require_type::require_java_method(func_symbol.type);
133135

134136
THEN("It has parameter x pointing to Generic")
135137
{
@@ -193,7 +195,8 @@ SCENARIO(
193195

194196
const symbolt func_symbol =
195197
new_symbol_table.lookup_ref(process_func_name);
196-
const java_method_typet func_code = require_type::require_code(func_symbol.type);
198+
const java_method_typet func_code =
199+
require_type::require_java_method(func_symbol.type);
197200

198201
THEN("It has parameter s pointing to Generic")
199202
{
@@ -258,7 +261,8 @@ SCENARIO(
258261

259262
const symbolt func_symbol =
260263
new_symbol_table.lookup_ref(process_func_name);
261-
const java_method_typet func_code = require_type::require_code(func_symbol.type);
264+
const java_method_typet func_code =
265+
require_type::require_java_method(func_symbol.type);
262266

263267
THEN("It has parameter inner pointing to Inner")
264268
{

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -317,7 +317,7 @@ SCENARIO(
317317
new_symbol_table.lookup_ref(process_func_name);
318318

319319
const java_method_typet &function_call =
320-
require_type::require_code(function_symbol.type, 2);
320+
require_type::require_java_method(function_symbol.type, 2);
321321

322322
THEN("The inputs are of correct type")
323323
{
@@ -346,7 +346,7 @@ SCENARIO(
346346
new_symbol_table.lookup_ref(process_func_name);
347347

348348
const java_method_typet &function_call =
349-
require_type::require_code(function_symbol.type, 3);
349+
require_type::require_java_method(function_symbol.type, 3);
350350

351351
THEN("The inputs are of correct type")
352352
{
@@ -382,7 +382,7 @@ SCENARIO(
382382
new_symbol_table.lookup_ref(process_func_name);
383383

384384
const java_method_typet &function_call =
385-
require_type::require_code(function_symbol.type, 2);
385+
require_type::require_java_method(function_symbol.type, 2);
386386

387387
THEN("The inputs are of correct type")
388388
{
@@ -413,7 +413,7 @@ SCENARIO(
413413
new_symbol_table.lookup_ref(process_func_name);
414414

415415
const java_method_typet &function_call =
416-
require_type::require_code(function_symbol.type, 2);
416+
require_type::require_java_method(function_symbol.type, 2);
417417

418418
THEN("The inputs are of correct type")
419419
{
@@ -443,7 +443,7 @@ SCENARIO(
443443
new_symbol_table.lookup_ref(process_func_name);
444444

445445
const java_method_typet &function_call =
446-
require_type::require_code(function_symbol.type, 2);
446+
require_type::require_java_method(function_symbol.type, 2);
447447

448448
THEN("The inputs are of correct type")
449449
{
@@ -477,7 +477,7 @@ SCENARIO(
477477
new_symbol_table.lookup_ref(process_func_name);
478478

479479
const java_method_typet &function_call =
480-
require_type::require_code(function_symbol.type, 2);
480+
require_type::require_java_method(function_symbol.type, 2);
481481

482482
THEN("The inputs are of correct type")
483483
{
@@ -509,7 +509,7 @@ SCENARIO(
509509
new_symbol_table.lookup_ref(process_func_name);
510510

511511
const java_method_typet &function_call =
512-
require_type::require_code(function_symbol.type, 2);
512+
require_type::require_java_method(function_symbol.type, 2);
513513

514514
THEN("The inputs are of correct type")
515515
{
@@ -545,7 +545,7 @@ SCENARIO(
545545
new_symbol_table.lookup_ref(process_func_name);
546546

547547
const java_method_typet &function_call =
548-
require_type::require_code(function_symbol.type, 2);
548+
require_type::require_java_method(function_symbol.type, 2);
549549

550550
THEN("The inputs are of correct type")
551551
{
@@ -577,7 +577,7 @@ SCENARIO(
577577
new_symbol_table.lookup_ref(process_func_name);
578578

579579
const java_method_typet &function_call =
580-
require_type::require_code(function_symbol.type, 2);
580+
require_type::require_java_method(function_symbol.type, 2);
581581

582582
THEN("The inputs are of the correct type")
583583
{
@@ -610,7 +610,7 @@ SCENARIO(
610610
new_symbol_table.lookup_ref(process_func_name);
611611

612612
const java_method_typet &function_call =
613-
require_type::require_code(function_symbol.type, 2);
613+
require_type::require_java_method(function_symbol.type, 2);
614614

615615
THEN("The inputs are of the correct type")
616616
{
@@ -643,7 +643,7 @@ SCENARIO(
643643
new_symbol_table.lookup_ref(process_func_name);
644644

645645
const java_method_typet &function_call =
646-
require_type::require_code(function_symbol.type, 2);
646+
require_type::require_java_method(function_symbol.type, 2);
647647

648648
THEN("The inputs should be of the correct type")
649649
{
@@ -673,7 +673,7 @@ SCENARIO(
673673
new_symbol_table.lookup_ref(process_func_name);
674674

675675
const java_method_typet &function_call =
676-
require_type::require_code(function_symbol.type, 1);
676+
require_type::require_java_method(function_symbol.type, 1);
677677

678678
THEN("The return type should be correct")
679679
{
@@ -700,7 +700,7 @@ SCENARIO(
700700
new_symbol_table.lookup_ref(process_func_name);
701701

702702
const java_method_typet &function_call =
703-
require_type::require_code(function_symbol.type, 1);
703+
require_type::require_java_method(function_symbol.type, 1);
704704

705705
THEN("The return type should be correct")
706706
{
@@ -730,7 +730,7 @@ SCENARIO(
730730
new_symbol_table.lookup_ref(process_func_name);
731731

732732
const java_method_typet &function_call =
733-
require_type::require_code(function_symbol.type, 1);
733+
require_type::require_java_method(function_symbol.type, 1);
734734

735735
THEN("The return type should be correct")
736736
{
@@ -759,7 +759,7 @@ SCENARIO(
759759
new_symbol_table.lookup_ref(process_func_name);
760760

761761
const java_method_typet &function_call =
762-
require_type::require_code(function_symbol.type, 1);
762+
require_type::require_java_method(function_symbol.type, 1);
763763

764764
THEN("The return type should be correct")
765765
{
@@ -791,7 +791,7 @@ SCENARIO(
791791
new_symbol_table.lookup_ref(process_func_name);
792792

793793
const java_method_typet &function_call =
794-
require_type::require_code(function_symbol.type, 1);
794+
require_type::require_java_method(function_symbol.type, 1);
795795

796796
THEN("The return type should be correct")
797797
{
@@ -821,7 +821,7 @@ SCENARIO(
821821
new_symbol_table.lookup_ref(process_func_name);
822822

823823
const java_method_typet &function_call =
824-
require_type::require_code(function_symbol.type, 1);
824+
require_type::require_java_method(function_symbol.type, 1);
825825

826826
THEN("The return type should be correct")
827827
{
@@ -855,7 +855,7 @@ SCENARIO(
855855
new_symbol_table.lookup_ref(process_func_name);
856856

857857
const java_method_typet &function_call =
858-
require_type::require_code(function_symbol.type, 1);
858+
require_type::require_java_method(function_symbol.type, 1);
859859

860860
THEN("The return type should be correct")
861861
{
@@ -886,7 +886,7 @@ SCENARIO(
886886
new_symbol_table.lookup_ref(process_func_name);
887887

888888
const java_method_typet &function_call =
889-
require_type::require_code(function_symbol.type, 1);
889+
require_type::require_java_method(function_symbol.type, 1);
890890

891891
THEN("The return type should be correct")
892892
{
@@ -918,7 +918,7 @@ SCENARIO(
918918
new_symbol_table.lookup_ref(process_func_name);
919919

920920
const java_method_typet &function_call =
921-
require_type::require_code(function_symbol.type, 1);
921+
require_type::require_java_method(function_symbol.type, 1);
922922

923923
THEN("The return type should be correct")
924924
{
@@ -950,7 +950,7 @@ SCENARIO(
950950
new_symbol_table.lookup_ref(process_func_name);
951951

952952
const java_method_typet &function_call =
953-
require_type::require_code(function_symbol.type, 1);
953+
require_type::require_java_method(function_symbol.type, 1);
954954

955955
THEN("The return type should be correct")
956956
{

0 commit comments

Comments
 (0)