Merge pull request #469 from mgudemann/fix_nondet_sublass_init_non_null

Daniel Kroening · web-flow · commit 30f73f5704af · 2017-01-31T17:23:19.000Z
Fix nondet sublass init non null
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
@@ -189,8 +189,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);

Original file line number	Diff line number	Diff line change
`@@ -189,8 +189,9 @@ void java_object_factoryt::gen_nondet_init(`
`189`	`189`	`{`
`190`	`190`	`const struct_typet &struct_type=to_struct_type(subtype);`
`191`	`191`	`const irep_idt struct_tag=struct_type.get_tag();`
`192`		`-`
`193`		`- if(recursion_set.find(struct_tag)!=recursion_set.end())`
	`192`	`+ // set to null if found in recursion set and not a sub-type`
	`193`	`+ if(recursion_set.find(struct_tag)!=recursion_set.end() &&`
	`194`	`+ struct_tag==class_identifier)`
`194`	`195`	`{`
`195`	`196`	`// make null`
`196`	`197`	`null_pointer_exprt null_pointer_expr(pointer_type);`