Update jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

tautschnig · Daniel Kroening · commit 1a512c172dc6 · 2018-10-18T10:02:17.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -88,7 +88,7 @@ static const std::string get_thread_block_identifier(
   const exprt &expr = f_code.arguments()[0];
   mp_integer lbl_id;
   if(to_integer(to_constant_expr(expr.op0()), lbl_id))
-    CHECK_RETURN(false);
+mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
   return integer2string(lbl_id);
 }
 

Original file line number	Diff line number	Diff line change
`@@ -88,7 +88,7 @@ static const std::string get_thread_block_identifier(`
`88`	`88`	`const exprt &expr = f_code.arguments()[0];`
`89`	`89`	`mp_integer lbl_id;`
`90`	`90`	`if(to_integer(to_constant_expr(expr.op0()), lbl_id))`
`91`		`- CHECK_RETURN(false);`
	`91`	`+mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());`
`92`	`92`	`return integer2string(lbl_id);`
`93`	`93`	`}`
`94`	`94`