comment

Daniel Kroening · Daniel Kroening · commit 2c8068669a71 · 2016-06-23T22:11:50.000+01:00
diff --git a/src/java_bytecode/java_bytecode_convert.cpp b/src/java_bytecode/java_bytecode_convert.cpp
@@ -781,6 +781,9 @@ codet java_bytecode_convertt::convert_instructions(
     }
     else if(statement=="checkcast")
     {
+      // checkcast throws an exception in case a cast of object
+      // on stack to given type fails.
+      // The stack isn't modified.
       assert(op.size()==1 && results.size()==1);
       results[0]=op[0];
     }

Original file line number	Diff line number	Diff line change
`@@ -781,6 +781,9 @@ codet java_bytecode_convertt::convert_instructions(`
`781`	`781`	`}`
`782`	`782`	`else if(statement=="checkcast")`
`783`	`783`	`{`
	`784`	`+ // checkcast throws an exception in case a cast of object`
	`785`	`+ // on stack to given type fails.`
	`786`	`+ // The stack isn't modified.`
`784`	`787`	`assert(op.size()==1 && results.size()==1);`
`785`	`788`	`results[0]=op[0];`
`786`	`789`	`}`