1) Further updates to specifications.

[repair.git] / Repair / RepairCompiler / MCC / specs / filesystem / test3.constraints

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 0b4dc230777f185e2b90c9a3a1fd3b5a437a3696..39d44626db78a758c41f02151d1b4a589ab21b0a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
@@ -8,46 +8,38 @@
 // C1
 // for all used inodes, verify that the inodestatus (built from the
 // inodebitmap is marked 'used'
-//[forall u in UsedInode], u.inodestatus=true;
+[forall u in UsedInode], u.inodestatus=true;
 
 // C2
 // for all free inodes, verify that the inodestatus (built from the 
 // inodebitmap is marked 'free'
-//[forall f in FreeInode], f.inodestatus=false;
+[forall f in FreeInode], f.inodestatus=false;
 
 // C3
 // for all used blocks, verify that the blockstatus (built from the
 // blockbitmap is marked 'used'
-//[forall u in UsedBlock], u.blockstatus=true;
+[forall u in UsedBlock], u.blockstatus=true;
 
 // C4
 // for all free blocks, verify that the blockstatus (built from the
 // block bitmap is marked 'free'
-//[forall f in FreeBlock], f.blockstatus=false;
+[forall f in FreeBlock], f.blockstatus=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);
+[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)*8192;
+[forall i in UsedInode], i.filesize <= sizeof(i.contents)*8192;
 
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block
-//[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
-
-// C8
-// verify that there is one superblock
-//[],sizeof(SuperBlock)=1;
-
-// C9
-// verify that there is one groupblock
-//[],sizeof(GroupBlock)=1;
+[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
 
 // C10
 // verify that there is one inodetableblock
@@ -63,4 +55,4 @@
 
 // C13
 // verify that there is one rootdirectoryinode
-//[],sizeof(RootDirectoryInode)=1;
+[],sizeof(RootDirectoryInode)=1;