Repair/RepairInterpreter/testconcrete

   1 [forall u in InodeTableBlock], true => d.g.InodeTableBlock=u
   2 [forall u in InodeBitmapBlock], true => d.g.InodeBitmapBlock=u
   3 [forall u in BlockBitmapBlock], true => d.g.BlockBitmapBlock=u
   4 [forall u in RootDirectoryInode], true => d.s.RootDirectoryInode=u
   5 [forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)], j < sizeof(i.contents) => cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=element j of i.contents
   6 [forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)], !j<sizeof(i.contents) => cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)
   7 [forall ibb in InodeBitmapBlock, forall <j,status> in inodestatus], status=literal(Free) => cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false)
   8 [forall ibb in InodeBitmapBlock, forall <j,status> in inodestatus], status=literal(Used) => cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true)
   9 [forall <de, u> in inodeof], true => de.inodenumber=u
  10 [forall itb in InodeTableBlock, forall <j,u> in referencecount], true => cast(InodeTable,d.b[itb]).itable[j].referencecount=u
  11 [forall itb in InodeTableBlock, forall <j,u> in filesize], true => cast(InodeTable,d.b[itb]).itable[j].filesize=u
  12 [forall bbb in BlockBitmapBlock, forall <j, status> in blockstatus], status=literal(Free) => cast(BlockBitmap,d.b[bbb]).blockbitmap[j] = literal(false)
  13 [forall bbb in BlockBitmapBlock, forall <j,status> in blockstatus], status=literal(Used) => cast(BlockBitmap,d.b[bbb]).blockbitmap[j] = literal(true)