fix type operand of instanceof

Daniel Kroening · Daniel Kroening · commit 238d7b80a525 · 2019-07-10T21:23:48.000+01:00
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
@@ -361,7 +361,9 @@ std::string expr2javat::convert_java_instanceof(const exprt &src)
     return convert_norep(src, precedence);
   }
 
-  return convert(src.op0())+" instanceof "+convert(src.op1().type());
+  const auto type = java_reference_type(to_struct_tag_type(src.op1().type()));
+
+  return convert(src.op0()) + " instanceof " + convert(type);
 }
 
 std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)

Original file line number	Diff line number	Diff line change
`@@ -361,7 +361,9 @@ std::string expr2javat::convert_java_instanceof(const exprt &src)`
`361`	`361`	`return convert_norep(src, precedence);`
`362`	`362`	`}`
`363`	`363`
`364`		`- return convert(src.op0())+" instanceof "+convert(src.op1().type());`
	`364`	`+ const auto type = java_reference_type(to_struct_tag_type(src.op1().type()));`
	`365`	`+`
	`366`	`+ return convert(src.op0()) + " instanceof " + convert(type);`
`365`	`367`	`}`
`366`	`368`
`367`	`369`	`std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)`