Merge pull request #598 from smowton/sss_checkcast

Daniel Kroening · web-flow · commit 921fdfdbffc6 · 2017-03-07T19:23:39.000-08:00
Java checkcast: fix stack when check disabled
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1030,10 +1030,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
         c=code_assertt(check);
         c.add_source_location().set_comment("Dynamic cast check");
         c.add_source_location().set_property_class("bad-dynamic-cast");
-        results[0]=op[0];
       }
       else
         c=code_skipt();
+
+      results[0]=op[0];
     }
     else if(statement=="invokedynamic")
     {

Original file line number	Diff line number	Diff line change
`@@ -1030,10 +1030,11 @@ codet java_bytecode_convert_methodt::convert_instructions(`
`1030`	`1030`	`c=code_assertt(check);`
`1031`	`1031`	`c.add_source_location().set_comment("Dynamic cast check");`
`1032`	`1032`	`c.add_source_location().set_property_class("bad-dynamic-cast");`
`1033`		`- results[0]=op[0];`
`1034`	`1033`	`}`
`1035`	`1034`	`else`
`1036`	`1035`	`c=code_skipt();`
	`1036`	`+`
	`1037`	`+ results[0]=op[0];`
`1037`	`1038`	`}`
`1038`	`1039`	`else if(statement=="invokedynamic")`
`1039`	`1040`	`{`