forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Adding a unit test for implicitly generic classes
- Loading branch information
1 parent
ba05f18
commit 0163362
Showing
11 changed files
with
305 additions
and
3 deletions.
There are no files selected for viewing
Binary file added
BIN
+848 Bytes
...bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class
Binary file not shown.
Binary file added
BIN
+900 Bytes
...ava_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class
Binary file not shown.
Binary file added
BIN
+821 Bytes
...bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class
Binary file not shown.
Binary file added
BIN
+774 Bytes
unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class
Binary file not shown.
Binary file added
BIN
+616 Bytes
...java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class
Binary file not shown.
Binary file added
BIN
+1.08 KB
unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class
Binary file not shown.
29 changes: 29 additions & 0 deletions
29
unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
class GenericClassWithInnerClasses<T> | ||
{ | ||
class Inner { | ||
T t1; | ||
Generic<T> t2; | ||
|
||
class InnerInner { | ||
T tt1; | ||
Generic<Generic<T>> tt2; | ||
} | ||
} | ||
|
||
class GenericInner<U> { | ||
T gt1; | ||
GenericTwoParam<T,U> gt2; | ||
|
||
class GenericInnerInner<V>{ | ||
|
||
} | ||
} | ||
|
||
static class StaticInner<U>{ | ||
U st; | ||
} | ||
|
||
Inner f1; | ||
Inner.InnerInner f2; | ||
GenericInner<Integer> f3; | ||
} |
219 changes: 219 additions & 0 deletions
219
unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,219 @@ | ||
/*******************************************************************\ | ||
Module: Unit tests for parsing generic classes | ||
Author: DiffBlue Limited. All rights reserved. | ||
\*******************************************************************/ | ||
|
||
#include <testing-utils/catch.hpp> | ||
#include <testing-utils/load_java_class.h> | ||
#include <testing-utils/require_type.h> | ||
|
||
SCENARIO( | ||
"parse_generic_class_with_inner_classes", | ||
"[core][java_bytecode][java_bytecode_parse_generics]") | ||
{ | ||
const symbol_tablet &new_symbol_table = load_java_class( | ||
"GenericClassWithInnerClasses", | ||
"./java_bytecode/java_bytecode_parse_generics"); | ||
|
||
std::string outer_class_prefix = "java::GenericClassWithInnerClasses"; | ||
|
||
WHEN("Generic outer class has fields which are objects of the inner classes") | ||
{ | ||
REQUIRE(new_symbol_table.has_symbol(outer_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(outer_class_prefix); | ||
const java_generic_class_typet &generic_class = | ||
require_type::require_java_generic_class( | ||
class_symbol.type, {outer_class_prefix + "::T"}); | ||
THEN("There is a field f1 of generic type with correct arguments") | ||
{ | ||
const auto &field = require_type::require_component(generic_class, "f1"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet(outer_class_prefix + "$Inner")); | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); | ||
} | ||
THEN("There is a field f2 of generic type with correct arguments") | ||
{ | ||
const auto &field = require_type::require_component(generic_class, "f2"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet(outer_class_prefix + "$Inner$InnerInner")); | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); | ||
} | ||
THEN("There is a field f3 of generic type with correct arguments") | ||
{ | ||
const auto &field = require_type::require_component(generic_class, "f3"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet(outer_class_prefix + "$GenericInner")); | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}, | ||
{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); | ||
} | ||
} | ||
|
||
WHEN("Inner class of a generic outer class is parsed") | ||
{ | ||
std::string inner_class_prefix = outer_class_prefix + "$Inner"; | ||
REQUIRE(new_symbol_table.has_symbol(inner_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(inner_class_prefix); | ||
|
||
THEN("It has correct implicit generic types") | ||
{ | ||
const java_implicitly_generic_class_typet &java_class = | ||
require_type::require_java_implicitly_generic_class( | ||
class_symbol.type, {outer_class_prefix + "::T"}); | ||
|
||
THEN( | ||
"There is a field t1 which is the generic parameter of the outer " | ||
"class") | ||
{ | ||
const auto &field = require_type::require_component(java_class, "t1"); | ||
require_type::require_java_generic_parameter( | ||
field.type(), outer_class_prefix + "::T"); | ||
} | ||
THEN( | ||
"There is a field t2 of generic type with the generic " | ||
"parameter of the outer class") | ||
{ | ||
const auto &field = require_type::require_component(java_class, "t2"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet("java::Generic")); | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Var, | ||
outer_class_prefix + "::T"}}); | ||
} | ||
} | ||
} | ||
|
||
WHEN("Inner class of an inner class of a generic outer class is parsed") | ||
{ | ||
std::string inner_inner_class_prefix = | ||
outer_class_prefix + "$Inner$InnerInner"; | ||
REQUIRE(new_symbol_table.has_symbol(inner_inner_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(inner_inner_class_prefix); | ||
|
||
THEN("It has correct implicit generic types") | ||
{ | ||
const java_implicitly_generic_class_typet &java_class = | ||
require_type::require_java_implicitly_generic_class( | ||
class_symbol.type, {outer_class_prefix + "::T"}); | ||
|
||
THEN( | ||
"There is a field tt1 which is the generic parameter of the outer " | ||
"class") | ||
{ | ||
const auto &field = require_type::require_component(java_class, "tt1"); | ||
require_type::require_java_generic_parameter( | ||
field.type(), outer_class_prefix + "::T"); | ||
} | ||
THEN( | ||
"There is a field tt2 of nested generic type with the generic " | ||
"parameter of the outer class") | ||
{ | ||
const auto &field = require_type::require_component(java_class, "tt2"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet("java::Generic")); | ||
const java_generic_typet &generic_field = | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Inst, "java::Generic"}}); | ||
|
||
const typet &type_argument = | ||
generic_field.generic_type_arguments().at(0); | ||
const java_generic_typet generic_type_argument = | ||
require_type::require_java_generic_type( | ||
type_argument, | ||
{{require_type::type_argument_kindt::Var, | ||
outer_class_prefix + "::T"}}); | ||
} | ||
} | ||
} | ||
|
||
WHEN("Generic inner class of a generic outer class is parsed") | ||
{ | ||
std::string generic_inner_class_prefix = | ||
outer_class_prefix + "$GenericInner"; | ||
REQUIRE(new_symbol_table.has_symbol(generic_inner_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(generic_inner_class_prefix); | ||
|
||
THEN("It has correct generic types and implicit generic types") | ||
{ | ||
require_type::require_java_implicitly_generic_class( | ||
class_symbol.type, {outer_class_prefix + "::T"}); | ||
const java_generic_class_typet &generic_class = | ||
require_type::require_java_generic_class( | ||
class_symbol.type, {generic_inner_class_prefix + "::U"}); | ||
|
||
THEN( | ||
"There is a field gt1 which is the generic parameter of the outer " | ||
"class") | ||
{ | ||
const auto &field = | ||
require_type::require_component(generic_class, "gt1"); | ||
require_type::require_java_generic_parameter( | ||
field.type(), outer_class_prefix + "::T"); | ||
} | ||
THEN( | ||
"There is a field gt2 of generic type with the generic " | ||
"parameter of the outer class") | ||
{ | ||
const auto &field = | ||
require_type::require_component(generic_class, "gt2"); | ||
require_type::require_pointer( | ||
field.type(), symbol_typet("java::GenericTwoParam")); | ||
require_type::require_java_generic_type( | ||
field.type(), | ||
{{require_type::type_argument_kindt::Var, | ||
outer_class_prefix + "::T"}, | ||
{require_type::type_argument_kindt::Var, | ||
generic_inner_class_prefix + "::U"}}); | ||
} | ||
} | ||
} | ||
|
||
WHEN( | ||
"A generic inner class of a generic inner class of a generic outer class " | ||
"is parsed") | ||
{ | ||
std::string generic_inner_inner_class_prefix = | ||
outer_class_prefix + "$GenericInner$GenericInnerInner"; | ||
REQUIRE(new_symbol_table.has_symbol(generic_inner_inner_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(generic_inner_inner_class_prefix); | ||
|
||
THEN("It has correct generic types and implicit generic types") | ||
{ | ||
require_type::require_java_implicitly_generic_class( | ||
class_symbol.type, | ||
{outer_class_prefix + "::T", outer_class_prefix + "$GenericInner::U"}); | ||
require_type::require_java_generic_class( | ||
class_symbol.type, {generic_inner_inner_class_prefix + "::V"}); | ||
} | ||
} | ||
|
||
WHEN("A static generic inner class of a generic class is parsed") | ||
{ | ||
std::string static_inner_class_prefix = outer_class_prefix + "$StaticInner"; | ||
REQUIRE(new_symbol_table.has_symbol(static_inner_class_prefix)); | ||
const symbolt &class_symbol = | ||
new_symbol_table.lookup_ref(static_inner_class_prefix); | ||
|
||
THEN("It has correct generic types and no implicit generic types") | ||
{ | ||
REQUIRE(!is_java_implicitly_generic_class_type(class_symbol.type)); | ||
require_type::require_java_generic_class( | ||
class_symbol.type, {static_inner_class_prefix + "::U"}); | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters