*&p is not equivalent to p

[necto]

Rather unexpected difference of two terms: p and *&p for a local variable void* p;. For some reason VeriFast does not allow direct use of p and prefers *&p |-> ?x; x instead. Here is the full code:

/*@ predicate myp(void* p); 
@*/

void init(void** pp);
//@ requires true;
//@ ensures *pp |-> ?p &*& myp(p);

int main()
//@ requires true;
//@ ensures true;
{
  void* p;
  init(&p);
  //@ assert *&p |-> ?x;
  //@ assert myp(x);//<-- this is fine
  //@ assert myp(p);//<-- Cannot perform dereference in this context.
}

Why is there a difference?

[btj]

There is no difference. VeriFast does not allow //@ assert myp(*&p); either, for the same reason that it does not allow //@ assert myp(foo->bar);: VeriFast does not allow heap-dependent expressions (in the broad sense of "heap": addressable memory) in assertions (and neither does separation logic) as a way to make sure that an assertion depends only on memory whose presence it asserts.

Note that VeriFast does accept //@ assert p |-> ?x;.

[necto]

I see. I guess my confusion arises actually from the fact that a seemingly side-effect free operation (&) breaks the following code. Here is a slightly different example:

/*@ predicate myp(void* p) = true;  @*/

void main()
//@ requires true;
//@ ensures myp(_);
{
  void* p;
  //@ close myp(p);
  // @ assert *&p |-> ?x; //<-- uncomment this, and you'll get
                          // "Cannot perform dereference in this context" on the next line
  //@ assert myp(p);
}

Here the last assert passes unless I take an address of p, which seems counterintuitive to me.