Support for inttoptr not implemented about smack HOT 4 CLOSED

OK, handling ptrtoint as well, while we're at it.

from smack.

The way i2p and p2i are implemented right now, SMACK reports a false bug for this example:
int main(void){
int x = (int)malloc(sizeof(int));
long y = (int)x;
int z = (int)y;

_x = 5;
__SMACK_assert(_z == 5);
}

I wonder if i2p and p2i should be just noops? Any good reason not to have them as noops?

from smack.

I'm not really sure about this one. If we treat i2p and p2i as no-ops, then any arithmetic on integers derived from the pointers becomes weird, since arithmetic uses only the "offset" component. I'm not really sure where this problem might manifest in practice, but consider the following program:

int _p = malloc(..);
*p = 0;
int x = (int) p;
int y = x + 1;
int z = y - 1;
int *q = (int *) z;
// here p and q alias, since x == z
*q = 5;
assert (_p == 0);
// this assertion does not hold.

Our translation, treating i2p and p2i as no-ops would work as follows:
p := $ptr(R,0);
x := $ptr(R,0);
y := $ptr(NULL,1);
z := $ptr(NULL,0);
q := $ptr(NULL,0);
// here p and q do not alias...
$Mem[q] := 5;
assert ($Mem[p] == 0);
// this assertion holds

The way our translation works now flags this as an error.
p := $ptr(R,0);
x := $ptr(NULL,0);
y := $ptr(NULL,1);
z := $ptr(NULL,0);
q := $ptr(S,0);
// here p and q MAY alias, given that R and S can be equal
$Mem[q] := 5;
assert ($Mem[p] == 0);
// this assertion may not hold

M

from smack.

I agree with your point. What we are doing now is sound, which is great and is probably good enough for most of real-world examples. Handling i2p/p2i precisely without having a good need for that does not make sense at this point. So let's just issue a warning that it is not handled precisely and that's it.

from smack.