Skip to content

Commit 7b17821

Browse files
committed
Add unit test verifying that java_object_factory doesn't strip tag types
Previously if asked to populate a pointer with tagged type (e.g. "Object *") then it would allocate a "struct Object { ... }", i.e. the struct_typet rather than the struct_tag_typet. This verifies that it now retains tag types.
1 parent 2ecdc0e commit 7b17821

19 files changed

+271
-0
lines changed

jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
4444
java_bytecode/java_bytecode_parser/parse_java_class.cpp \
4545
java_bytecode/java_bytecode_parser/parse_java_field.cpp \
4646
java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
47+
java_bytecode/java_object_factory/struct_tag_types.cpp \
4748
java_bytecode/java_replace_nondet/replace_nondet.cpp \
4849
java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
4950
java_bytecode/java_types/erase_type_arguments.cpp \
264 Bytes
Binary file not shown.
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
2+
public class A {
3+
4+
public B b;
5+
public C c;
6+
7+
}
8+
9+
class B { }
10+
11+
class C { }
228 Bytes
Binary file not shown.
228 Bytes
Binary file not shown.
235 Bytes
Binary file not shown.
849 Bytes
Binary file not shown.
Binary file not shown.
Binary file not shown.
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
2+
public class HasArray {
3+
4+
public D[] ds;
5+
6+
}
7+
8+
class D { }

0 commit comments

Comments
 (0)