Added array analysis (computes paths used to add elements/tuples to sets/relations.

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

diff --git a/Repair/RepairCompiler/MCC/test2.constraints b/Repair/RepairCompiler/MCC/test2.constraints
index 44e92f65909a291d151185a94dce7e62ce111a02..bbc92e4458149d8dc06a74c219eaa90bb644ba32 100755 (executable)
--- a/Repair/RepairCompiler/MCC/test2.constraints
+++ b/Repair/RepairCompiler/MCC/test2.constraints
@@ -8,50 +8,50 @@
 // C1
 // for all used inodes, verify that the inodestatus (built from the
 // inodebitmap is marked 'used'
-[forall u in UsedInode], u.inodestatus=literal(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(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(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(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);
+//[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);
+//[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);
+//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
 
 // C8
 // verify that there is one superblock
-[],sizeof(SuperBlock)=literal(1);
+//[],sizeof(SuperBlock)=literal(1);
 
 // C9
 // verify that there is one groupblock
-[],sizeof(GroupBlock)=literal(1);
+//[],sizeof(GroupBlock)=literal(1);
 
 // C10
 // verify that there is one inodetableblock
-[],sizeof(InodeTableBlock)=literal(1);
+//[],sizeof(InodeTableBlock)=literal(1);
 
 // C11
 // verify that there is one inodebitmapblock 
@@ -59,8 +59,8 @@
 
 // C12
 // verify that there is one blockbitmapblock
-[],sizeof(BlockBitmapBlock)=literal(1);
+//[],sizeof(BlockBitmapBlock)=literal(1);
 
 // C13
 // verify that there is one rootdirectoryinode
-[],sizeof(RootDirectoryInode)=literal(1);
+//[],sizeof(RootDirectoryInode)=literal(1);