Skip to content

Commit e2e2360

Browse files
committed
Add test for Java integers with --no-simplify
See issue cbmc#1015 for detail.
1 parent 30866b5 commit e2e2360

File tree

4 files changed

+21
-5
lines changed

4 files changed

+21
-5
lines changed
Binary file not shown.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--no-simplify --function test.f --cover location
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
2+
public class test {
3+
4+
public void f() {
5+
6+
int x = 50;
7+
8+
}
9+
10+
}

src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1417,11 +1417,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
14171417
else if(statement==patternt("?ipush"))
14181418
{
14191419
assert(results.size()==1);
1420-
namespacet ns(symbol_table);
1421-
// Force a simplify here in case we have --no-simplify
1422-
// because the simplifier is the only pass that knows how to
1423-
// deal with this cast from integer_typet:
1424-
results[0]=simplify_expr(typecast_exprt(arg0, java_int_type()), ns);
1420+
mp_integer int_value;
1421+
bool ret=to_integer(to_constant_expr(arg0), int_value);
1422+
INVARIANT(!ret, "?ipush argument should be an integer");
1423+
results[0]=from_integer(int_value, java_int_type());
14251424
}
14261425
else if(statement==patternt("if_?cmp??"))
14271426
{

0 commit comments

Comments
 (0)