0b4dc230777f185e2b90c9a3a1fd3b5a437a3696
[repair.git] / 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)*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)=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;