struct X { bool a; };

struct Ptr { X* operator->(); };

//@ requires p->a;
void foo(Ptr p);