Description
The following program (run with -alltypes
) rewrites callee
's return type to _Ptr
, but it would seem like it should be _Array_Ptr
:
int *callee(int *a) { // BECOMES _Ptr<int> callee(int *a : itype(_Array_ptr<int>)) {
int *z = a; // BECOMES _Array_ptr<int> z = a;
z += 2;
return z;
}
void caller() {
int *y = malloc(sizeof(int));
callee(y);
}
The malloc
is creating a pointer to a single thing; the constraint on &&malloc_4
is PTR
. But then the constraint forces PTR --> .... --> ARR
on the blue edges, which is not satisfiable. As such, somehow y_3
is changed to WILD
but callee:a_0
and z_2
themselves are kept as ARR
.
I'm not sure why this happens, but here's a theory. See lines 250-282 in Constraints.cpp
(16fd8d1) and also 353-370, which check for failed constraints and change solutions. What might be happening is that the change to a WILD for &&malloc_4
flows on the red edges up through y_3
and then stops. But the blue edge from PTR
keeps going all the way to <<callee:$ret_1
.