Add two preconditions and it will always be "Verification succeeded"!!

May 11, 2015 at 8:57 AM
void vListInsert( xList *pxList, xListItem *pxNewListItem )
_(requires \wrapped(pxList))
_(requires \wrapped(pxNewListItem))

_(writes pxList)
_(writes \span(pxNewListItem))

_(ensures \wrapped(pxList))
_(ensures \nested(pxNewListItem))
_(ensures pxList->uxNumberOfItems == \old(pxList->uxNumberOfItems)+1)
{
int a = 1;
_(assert a == 0)
* ...*\
}

Verification of xLIST#adm succeeded. [1.15]
Verification of strnlen_s succeeded. [0.02]
Verification of wcsnlen_s succeeded. [0.00]
Verification of vListInsert succeeded. [0.03]

=== Verification succeeded. ===

This is a List insert function. And as long as I use the two _(requires \wrapped(pxList)) _(requires \wrapped(pxNewListItem)) preconditions,whatever I write in the function body,it will be verified successfully. In this case, _(assert a == 0) is absolutely wrong, but it still display "verification successed"...
I need your help to figure it out..
Developer
Jul 29, 2016 at 7:58 PM
It verifies because your preconditions are inconsistent.

A writes clause implicitly requires that any non-object in the list is mutable. Since you've required that pxNewListItem is wrapped, its fields can't be mutable. So these two clauses are inconsistent.

Whenever you get such an inconsistency, you should first try to see whether you can prove \false (or 0). If you can't figure out what's wrong with your preconditions, try writing a test function that has no preconditions and (after suitable preparation) calls the function with the problematic preconditions. This will usually show you what is going wrong. (In this case, you would be told that you are violating the precondition coming from the writes clause.)