Organizing

[repair.git] / Repair / RepairCompiler / MCC / test2.constraints

diff --git a/Repair/RepairCompiler/MCC/test2.constraints b/Repair/RepairCompiler/MCC/test2.constraints
deleted file mode 100755 (executable)
index bbc92e4..0000000
--- a/Repair/RepairCompiler/MCC/test2.constraints
+++ /dev/null
@@ -1,66 +0,0 @@
-// sEXT2 - Simple File System Example
-// Constraint Definition Language File
-
-// Constraints 1-4 verify that the bitmaps and references to block's match up
-// Constraints 5-6 verify that references counts and filesizes match up
-// Constraints 7-13 are singleton tests
-
-// C1
-// for all used inodes, verify that the inodestatus (built from the
-// inodebitmap is marked 'used'
-//[forall u in UsedInode], u.inodestatus=literal(true);
-
-// C2
-// for all free inodes, verify that the inodestatus (built from the 
-// inodebitmap is marked 'free'
-//[forall f in FreeInode], f.inodestatus=literal(false);
-
-// C3
-// for all used blocks, verify that the blockstatus (built from the
-// blockbitmap is marked 'used'
-//[forall u in UsedBlock], u.blockstatus=literal(true);
-
-// C4
-// for all free blocks, verify that the blockstatus (built from the
-// block bitmap is marked 'free'
-//[forall f in FreeBlock], f.blockstatus=literal(false);
-
-// C5
-// for all used inodes, verify that the reference count is equal to
-// the number of directory entries (files/links) that refer to that
-// inode
-//[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
-
-// C6
-// for all used inodes, verify that the filesize is consistent with
-// the number of blocks used (those in i.contents)
-//[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
-
-// C7
-// ??? for all files and directory blocks check that
-// only one inode references this block
-//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
-
-// C8
-// verify that there is one superblock
-//[],sizeof(SuperBlock)=literal(1);
-
-// C9
-// verify that there is one groupblock
-//[],sizeof(GroupBlock)=literal(1);
-
-// C10
-// verify that there is one inodetableblock
-//[],sizeof(InodeTableBlock)=literal(1);
-
-// C11
-// verify that there is one inodebitmapblock 
-[],sizeof(InodeBitmapBlock)=literal(1);
-
-// C12
-// verify that there is one blockbitmapblock
-//[],sizeof(BlockBitmapBlock)=literal(1);
-
-// C13
-// verify that there is one rootdirectoryinode
-//[],sizeof(RootDirectoryInode)=literal(1);