From 50d161cbb0c81eceb3354d923d3d3faae390a46d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 15 Dec 2016 12:51:10 +0100 Subject: [PATCH] ignore recursion set if class is subtype --- src/java_bytecode/java_object_factory.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index f8f3d98748f..35d4463a7ca 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -190,8 +190,9 @@ void java_object_factoryt::gen_nondet_init( { const struct_typet &struct_type=to_struct_type(subtype); const irep_idt struct_tag=struct_type.get_tag(); - - if(recursion_set.find(struct_tag)!=recursion_set.end()) + // set to null if found in recursion set and not a sub-type + if(recursion_set.find(struct_tag)!=recursion_set.end() && + struct_tag==class_identifier) { // make null null_pointer_exprt null_pointer_expr(pointer_type);