Open ArmborstL opened 1 month ago
When marking a C procedure as pure, one can add a unfold statement like below:
unfold
/*@ 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
with unfold
unfolding
(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.
list->next
The with unfold should either be translated into unfolding, or explicitly disallowed.
When marking a C procedure as pure, one can add a
unfoldstatement like below:This parses fine, so I'd expect that the
with unfoldgets translated to anunfolding. In reality, it is just dropped; the viper output isConsequently, VerCors reports There may be insufficient permission to dereference the pointer for the
list->next.The
with unfoldshould either be translated intounfolding, or explicitly disallowed.