Skip to content

Commit c63c05b

Browse files
author
svorenova
committed
Add unit tests for mocked/unsupported generics cont.
1 parent 067eeff commit c63c05b

File tree

8 files changed

+55
-48
lines changed

8 files changed

+55
-48
lines changed

‎unit/goto-programs/goto_program_generics/GenericBases.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ class SuperclassInnerUninstTest
9797
{
9898
SuperclassInnerUninst<IWrapper> f;
9999
public void foo() {
100-
IWrapper x = new IWrapper();
100+
IWrapper x = new IWrapper(0);
101101
f.inner.foo(x);
102102
f.inner_gen.foo(x,true);
103103
f.inner_three.foo(x);
@@ -110,7 +110,7 @@ public void foo() {
110110
}
111111
}
112112

113-
class SuperclassMocked extends MockedWrapper<IWrapper> {
113+
class SuperclassOpaque extends OpaqueWrapper<IWrapper> {
114114
public void foo() {
115115
this.field.i = 5;
116116
}

‎unit/goto-programs/goto_program_generics/GenericFieldMocked.class renamed to ‎unit/goto-programs/goto_program_generics/GenericFieldOpaque.class

535 Bytes
Binary file not shown.

‎unit/goto-programs/goto_program_generics/GenericFields.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,8 +106,8 @@ public void foo() {
106106
}
107107
}
108108

109-
class GenericFieldMocked {
110-
public MockedWrapper<IWrapper> f;
109+
class GenericFieldOpaque {
110+
public OpaqueWrapper<IWrapper> f;
111111
public void foo() {
112112
f.field.i = 0;
113113
}

‎unit/goto-programs/goto_program_generics/GenericHelper.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ class UnsupportedWrapper2<T extends InterfaceWrapper & InterfacePairWrapper>
4040
public T field;
4141
}
4242

43-
// generic mocked class, make sure the .class file is not available
44-
class MockedWrapper<T> {
43+
// generic opaque class, make sure the .class file is not available
44+
class OpaqueWrapper<T> {
4545
public T field;
4646
}

‎unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class

13 Bytes
Binary file not shown.

‎unit/goto-programs/goto_program_generics/SuperclassMocked.class renamed to ‎unit/goto-programs/goto_program_generics/SuperclassOpaque.class

465 Bytes
Binary file not shown.

‎unit/goto-programs/goto_program_generics/generic_bases_test.cpp

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
#include <testing-utils/require_goto_statements.h>
1111
#include <util/config.h>
1212
#include <testing-utils/require_type.h>
13+
#include <testing-utils/require_symbol.h>
1314

1415
// NOTE: To inspect these tests at any point, use expr2java.
1516
// A good way to verify the validity of a test is to iterate
@@ -430,26 +431,32 @@ SCENARIO(
430431
THEN("The struct for UnsupportedWrapper1 is complete and non-generic")
431432
{
432433
const std::string superclass_name = "java::UnsupportedWrapper1";
433-
REQUIRE(symbol_table.has_symbol(superclass_name));
434-
435434
const symbolt &superclass_symbol =
436-
symbol_table.lookup_ref(superclass_name);
437-
require_type::require_java_non_generic_class(superclass_symbol.type);
435+
require_symbol::require_symbol_exists(symbol_table, superclass_name);
436+
437+
require_type::require_complete_java_non_generic_class(
438+
superclass_symbol.type);
438439
}
439440

440441
WHEN("The method input argument is created in the entry point function")
441442
{
442443
const std::vector<codet> &entry_point_code =
443444
require_goto_statements::require_entry_point_statements(symbol_table);
444445

445-
// For an explanation of this part, look at the comments for the similar
446-
// parts of the previous tests.
446+
// We trace the creation of the object that is being supplied as
447+
// the input to the method under test. There must be one non-null
448+
// assignment only, and usually looks like this:
449+
// this = &tmp_object_factory$1;
447450
const irep_idt &this_tmp_name =
448451
require_goto_statements::require_entry_point_argument_assignment(
449452
"this", entry_point_code);
450453

451454
THEN("Object 'this' created has unspecialized inherited field")
452455
{
456+
// [email protected] =
457+
// &tmp_object_factory$2;
458+
// struct java.lang.Object { __CPROVER_string @class_identifier;
459+
// boolean @lock; } tmp_object_factory$2;
453460
require_goto_statements::require_struct_component_assignment(
454461
this_tmp_name,
455462
{"UnsupportedWrapper1"},
@@ -466,23 +473,18 @@ SCENARIO(
466473
"marked as generic)")
467474
{
468475
const symbol_tablet &symbol_table = load_java_class(
469-
"SuperclassMocked",
476+
"SuperclassOpaque",
470477
"./goto-programs/goto_program_generics",
471-
"SuperclassMocked.foo");
478+
"SuperclassOpaque.foo");
472479

473-
THEN("The struct for MockedWrapper is incomplete and not-generic")
480+
THEN("The struct for OpaqueWrapper is incomplete and not-generic")
474481
{
475-
const std::string superclass_name = "java::MockedWrapper";
476-
REQUIRE(symbol_table.has_symbol(superclass_name));
477-
482+
const std::string superclass_name = "java::OpaqueWrapper";
478483
const symbolt &superclass_symbol =
479-
symbol_table.lookup_ref(superclass_name);
480-
const java_class_typet &superclass_type =
481-
to_java_class_type(to_class_type(superclass_symbol.type));
482-
REQUIRE(
483-
to_class_type(superclass_symbol.type).get_bool(ID_incomplete_class));
484-
REQUIRE(!is_java_generic_class_type(superclass_type));
485-
REQUIRE(!is_java_implicitly_generic_class_type(superclass_type));
484+
require_symbol::require_symbol_exists(symbol_table, superclass_name);
485+
486+
require_type::require_incomplete_class(superclass_symbol.type);
487+
require_type::require_java_non_generic_class(superclass_symbol.type);
486488
}
487489

488490
WHEN("The method input argument is created in the entry point function")
@@ -500,7 +502,7 @@ SCENARIO(
500502
{
501503
require_goto_statements::require_struct_component_assignment(
502504
this_tmp_name,
503-
{"MockedWrapper"},
505+
{"OpaqueWrapper"},
504506
"field",
505507
"java::java.lang.Object",
506508
{},

‎unit/goto-programs/goto_program_generics/generic_parameters_test.cpp

Lines changed: 27 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
#include <testing-utils/require_goto_statements.h>
1111
#include <util/config.h>
1212
#include <testing-utils/require_type.h>
13+
#include <testing-utils/require_symbol.h>
1314

1415
// NOTE: To inspect these tests at any point, use expr2java.
1516
// A good way to verify the validity of a test is to iterate
@@ -504,18 +505,20 @@ SCENARIO(
504505

505506
THEN("The struct for UnsupportedWrapper2 is complete and non-generic")
506507
{
507-
const std::string superclass_name = "java::UnsupportedWrapper2";
508-
REQUIRE(symbol_table.has_symbol(superclass_name));
509-
508+
const std::string field_class_name = "java::UnsupportedWrapper2";
510509
const symbolt &superclass_symbol =
511-
symbol_table.lookup_ref(superclass_name);
512-
require_type::require_java_non_generic_class(superclass_symbol.type);
510+
require_symbol::require_symbol_exists(symbol_table, field_class_name);
511+
512+
require_type::require_complete_java_non_generic_class(
513+
superclass_symbol.type);
513514
}
514515

515516
WHEN("The method input argument is created in the entry point function")
516517
{
517-
// For an explanation of this part, look at the comments for the similar
518-
// parts of the previous tests.
518+
// We trace the creation of the object that is being supplied as
519+
// the input to the method under test. There must be one non-null
520+
// assignment only, and usually looks like this:
521+
// this = &tmp_object_factory$1;
519522
const std::vector<codet> &entry_point_code =
520523
require_goto_statements::require_entry_point_statements(symbol_table);
521524

@@ -525,6 +528,10 @@ SCENARIO(
525528

526529
THEN("Object 'this' has field 'f' of type UnsupportedWrapper2")
527530
{
531+
// tmp_object_factory$1.f = &tmp_object_factory$2;
532+
// struct UnsupportedWrapper2 { struct java.lang.Object
533+
// @java.lang.Object; struct java.lang.Object *field; }
534+
// tmp_object_factory$2;
528535
const auto &field_input_name =
529536
require_goto_statements::require_struct_component_assignment(
530537
tmp_object_name,
@@ -536,6 +543,9 @@ SCENARIO(
536543

537544
THEN("Object 'f' has unspecialized field 'field'")
538545
{
546+
// tmp_object_factory$2.field = &tmp_object_factory$3;
547+
// struct java.lang.Object { __CPROVER_string @class_identifier;
548+
// boolean @lock; } tmp_object_factory$3;
539549
require_goto_statements::require_struct_component_assignment(
540550
field_input_name,
541551
{},
@@ -553,23 +563,18 @@ SCENARIO(
553563
"incomplete and not marked as generic)")
554564
{
555565
const symbol_tablet &symbol_table = load_java_class(
556-
"GenericFieldMocked",
566+
"GenericFieldOpaque",
557567
"./goto-programs/goto_program_generics",
558-
"GenericFieldMocked.foo");
568+
"GenericFieldOpaque.foo");
559569

560-
THEN("The struct for MockedWrapper is incomplete and not-generic")
570+
THEN("The struct for OpaqueWrapper is incomplete and not-generic")
561571
{
562-
const std::string superclass_name = "java::MockedWrapper";
563-
REQUIRE(symbol_table.has_symbol(superclass_name));
572+
const std::string field_class_name = "java::OpaqueWrapper";
573+
const symbolt &field_class_symbol =
574+
require_symbol::require_symbol_exists(symbol_table, field_class_name);
564575

565-
const symbolt &superclass_symbol =
566-
symbol_table.lookup_ref(superclass_name);
567-
const java_class_typet &superclass_type =
568-
to_java_class_type(to_class_type(superclass_symbol.type));
569-
REQUIRE(
570-
to_class_type(superclass_symbol.type).get_bool(ID_incomplete_class));
571-
REQUIRE(!is_java_generic_class_type(superclass_type));
572-
REQUIRE(!is_java_implicitly_generic_class_type(superclass_type));
576+
require_type::require_incomplete_class(field_class_symbol.type);
577+
require_type::require_java_non_generic_class(field_class_symbol.type);
573578
}
574579

575580
WHEN("The method input argument is created in the entry point function")
@@ -583,14 +588,14 @@ SCENARIO(
583588
require_goto_statements::require_entry_point_argument_assignment(
584589
"this", entry_point_code);
585590

586-
THEN("Object 'this' has field 'f' of type MockedWrapper")
591+
THEN("Object 'this' has field 'f' of type OpaqueWrapper")
587592
{
588593
const auto &field_input_name =
589594
require_goto_statements::require_struct_component_assignment(
590595
tmp_object_name,
591596
{},
592597
"f",
593-
"java::MockedWrapper",
598+
"java::OpaqueWrapper",
594599
{},
595600
entry_point_code);
596601

0 commit comments

Comments
 (0)