Closed
Description
When checking for division by zero, the following shows different results when analyzing the static method f (passes the verification) and g (fails verification), although non-deterministic choice for the input integer should allow for a = -1 in the first case, too.
public class StaticMethod {
static public void f(int a, int b) {
int c = b/(a+1);
}
static public void g(int a, int b) {
int c = a/(b+1);
}
}
The problem seems to be that the first parameter that is passed to the static method is the result of a malloc, i.e., the memory allocated for a StaticMethod object instance. Whereas, in the function it is treated as a NONDET(int).
// 0 no location
__CPROVER_initialize();
// 1 no location
tmp_struct_init$1 = MALLOC(struct StaticMethod { struct java.lang.Object @java.lang.Object; }, 4);
// 2 no location
tmp_struct_init$1->@java.lang.Object.@class_identifier = "StaticMethod";
// 3 no location
StaticMethod.g:(II)V(tmp_struct_init$1, NONDET(int));
// 4 no location
END_FUNCTION
StaticMethod.f() /* java::StaticMethod.f:(II)V */
// 7 file StaticMethod.java line 4
ASSERT !(arg0i == -1) // division by zero in arg1i / (arg0i + 1)
// 8 file StaticMethod.java line 4
local2i = arg1i / (arg0i + 1);
// 9 no location
END_FUNCTION