This project is read-only.

Verifying C programs with nested structures

Mar 13, 2013 at 4:14 PM
I am trying to verify a 'C' program with nested structures. Suppose a structure 'A' contains a reference say 'ptrToBFromA' to another structure say 'B'. A's invariant first says 'A' owns 'ptrToBFromA'. The second invariant need to say something about a field say 'dataInC' of the pointer 'ptrToCFromB' in the structure 'B'. For instance consider the code given below

struct C{
     int data;

_(dynamic_owns) struct B{
    struct C *toC;
    _(invariant  ( toC!=0 )  && \mine(toC) )
    _(invariant  ( \mine(toC) )  ==>  ( toC->data>5 ) )

_(dynamic_owns) struct A{
   struct B *toB;
   _(invariant  (toB!=0) && \mine(toB) )
   _(invariant  ( \mine(toB) && \mine(toB->toC) )  ==>  ( toB->toC->data<10 ) )
    _(invariant  ( toC!=0 )  && \mine(toB->toC) ) //This is not possible as toC->\owner==toB

To say the second invariant in the structure 'A' I need to say if I own these pointers, then the property specified about the fields must hold. But as 'toC' is in the ownership of 'toB' saying '\mine(toB->toC)' implies something in structure 'A' is wrong.

Can somebody help me in solving this issue?
Mar 14, 2013 at 6:15 AM
In this case actually I can say
\mine(toB) and toC \in toB->\owns
as an invariant in the structure A.

But VCC gives some error message like "..forbids unwrapping .." when the nesting level is more and arrays are involved.


Sumesh Divakaran
Mar 25, 2013 at 12:06 AM
I may be mistaken on this, but objects only have one owner. An A object can't own toB->toC because toB->toC is already owned by toB.

Can you give a complete example involving C, B, and A objects which demonstrates why you are trying _(invariant ( toC!=0 ) && \mine(toB->toC) )?