"unfold" in pure method is silently dropped

[ArmborstL]

When marking a C procedure as pure, one can add a unfold statement like below:

/*@ pure*/ int size(struct node *list) {
    if(list==NULL) return 0;
    else return 1+/*@ with unfold state(list);*/size(list->next);
}

This parses fine, so I'd expect that the with unfold gets translated to an unfolding. In reality, it is just dropped; the viper output is

(some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer])) ?
    0 :
    1 + size1(ptrDeref(ptrAdd(optGet2(list), 0)).ref.next))

Consequently, VerCors reports There may be insufficient permission to dereference the pointer for the list->next.

The with unfold should either be translated into unfolding, or explicitly disallowed.