Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints

   1 // sEXT2 - Simple File System Example
   2 // Constraint Definition Language File
   3
   4 // Constraints 1-4 verify that the bitmaps and references to block's match up
   5 // Constraints 5-6 verify that references counts and filesizes match up
   6 // Constraints 7-13 are singleton tests
   7
   8 // C1
   9 // for all used inodes, verify that the inodestatus (built from the
  10 // inodebitmap is marked 'used'
  11 //[forall u in UsedInode], u.inodestatus=true;
  12
  13 // C2
  14 // for all free inodes, verify that the inodestatus (built from the
  15 // inodebitmap is marked 'free'
  16 //[forall f in FreeInode], f.inodestatus=false;
  17
  18 // C3
  19 // for all used blocks, verify that the blockstatus (built from the
  20 // blockbitmap is marked 'used'
  21 //[forall u in UsedBlock], u.blockstatus=true;
  22
  23 // C4
  24 // for all free blocks, verify that the blockstatus (built from the
  25 // block bitmap is marked 'free'
  26 [forall f in FreeBlock], f.blockstatus=false;
  27
  28 // C5
  29 // for all used inodes, verify that the reference count is equal to
  30 // the number of directory entries (files/links) that refer to that
  31 // inode
  32 //[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
  33
  34 // C6
  35 // for all used inodes, verify that the filesize is consistent with
  36 // the number of blocks used (those in i.contents)
  37 //[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
  38
  39 // C7
  40 // ??? for all files and directory blocks check that
  41 // only one inode references this block
  42 //[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
  43
  44 // C8
  45 // verify that there is one superblock
  46 //[],sizeof(SuperBlock)=1;
  47
  48 // C9
  49 // verify that there is one groupblock
  50 //[],sizeof(GroupBlock)=1;
  51
  52 // C10
  53 // verify that there is one inodetableblock
  54 /*[],sizeof(InodeTableBlock)=1;*/
  55
  56 // C11
  57 // verify that there is one inodebitmapblock
  58 /*[],sizeof(InodeBitmapBlock)=1;*/
  59
  60 // C12
  61 // verify that there is one blockbitmapblock
  62 [],sizeof(BlockBitmapBlock)=1;
  63
  64 // C13
  65 // verify that there is one rootdirectoryinode
  66 /*[],sizeof(RootDirectoryInode)=1;*/