# Verifying C programs with nested structures

 sumeshdivakaran Mar 13, 2013 at 3: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? sumeshdivakaran Mar 14, 2013 at 5: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. regards Sumesh Divakaran dtrebbien Mar 24, 2013 at 11:06 PM 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) )?