Repair/RepairCompiler/MCC/specs/abiword/abi.constraints

   1 [], sizeof(firstblock)=1;
   2 [], sizeof(Fragments)=1;
   3 [], sizeof(secondblock)=1;
   4 [forall f in Frags], (!(sizeof(f.Next)=1)) or ((f.Next.Prev=f) and sizeof(f.Next.Prev)=1);
   5 [forall f in Frags], (sizeof(f.~Next)<=1);
   6 [forall f in firstblock], sizeof(f.~Next)=0;
   7 [forall l in Last, forall f in Fragments], f.PLast=l and sizeof(f.PLast)=1;