[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
afs-base,
buffer-option
with
predicates pre-lookup : nat × dentry × dir-heap × file-heap;
pre-create : inode × dentry × metadata × dir-heap × file-heap;
pre-unlink : inode × inode × dentry × dir-heap × file-heap;
pre-mkdir : inode × dentry × metadata × dir-heap × file-heap;
pre-rmdir : inode × inode × dentry × dir-heap × file-heap;
pre-link : inode × inode × dentry × dentry × dir-heap × file-heap;
pre-rename : inode × dentry × inode × inode × dentry × inode × dir-heap × file-heap;
pre-readpage : inode × nat × buffer × dir-heap × file-heap;
pre-writepage : inode × nat × buffer × dir-heap × file-heap;
pre-evict : inode × dir-heap × file-heap;
pre-readdir : nat × dir-heap × file-heap;
pre-truncate : inode × nat × nat × buffer-opt × dir-heap × file-heap;
pre-iget : nat × dir-heap × file-heap;
pre-write-inode : inode × dir-heap × file-heap;
valid-dir-inode : inode × dir-heap × file-heap;
valid-file-inode : inode × dir-heap × file-heap;
valid-wb-inode : inode × dir-heap × file-heap;
variables old_ino : nat;
new_ino : nat;
pageno : nat;
old_dent : dentry;
new_dent : dentry;
p_inode : inode;
c_inode : inode;
new_inode : inode;
old_inode : inode;
new_dent_inode : inode;
old_dent_inode : inode;
old_parent_inode : inode;
new_parent_inode : inode;
old_child_inode : inode;
new_child_inode : inode;
axioms pre-lookup : ⊦ pre-lookup(p_ino, dent, dirs, files) ↔ valid-parent-ino(p_ino, dirs, files);
used for: ls, s, lss, ss;
pre-create
: ⊦ pre-create(p_inode, dent, md, dirs, files) ↔ valid-negdentry(p_inode.ino, dent, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files);
used for: ls, s, lss, ss;
pre-unlink
: ⊦ pre-unlink(p_inode, c_inode, dent, dirs, files)
↔ valid-dentry(p_inode.ino, dent, dirs, files) ∧ valid-file-inode(c_inode, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files)
∧ c_inode.ino = dent.ino;
used for: ls, s, lss, ss;
pre-mkdir
: ⊦ pre-mkdir(p_inode, dent, md, dirs, files) ↔ valid-negdentry(p_inode.ino, dent, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files);
used for: ls, s, lss, ss;
pre-rmdir
: ⊦ pre-rmdir(p_inode, c_inode, dent, dirs, files)
↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, dirs, files) ∧ dir-empty(dent.ino, dirs, files)
∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-dir-inode(c_inode, dirs, files) ∧ c_inode.ino = dent.ino;
used for: ls, s, lss, ss;
pre-link
: ⊦ pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files)
↔ valid-dentry(old_dent, dirs, files) ∧ valid-negdentry(p_inode.ino, new_dent, dirs, files)
∧ (links(old_dent.ino, dirs) ≠ ∅ ∨ old_dent.ino = ROOT_INO) ∧ valid-dir-inode(p_inode, dirs, files)
∧ valid-file-inode(c_inode, dirs, files) ∧ c_inode.ino = old_dent.ino;
used for: ls, s, lss, ss;
pre-rename
: ⊦ pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files)
↔ ( valid-negdentry(new_parent_inode.ino, new_dent, dirs, files)
∨ valid-dentry(new_parent_inode.ino, new_dent, dirs, files) ∧ valid-wb-inode(new_child_inode, dirs, files)
∧ new_child_inode.ino = new_dent.ino ∧ (valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files))
∧ (valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files)))
∧ valid-dentry(old_parent_inode.ino, old_dent, dirs, files) ∧ valid-dir-inode(old_parent_inode, dirs, files)
∧ valid-dir-inode(new_parent_inode, dirs, files)
∧ (new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta)
∧ valid-wb-inode(old_child_inode, dirs, files) ∧ old_child_inode.ino = old_dent.ino;
used for: ls, s, lss, ss;
pre-readpage : ⊦ pre-readpage(inode, n, buf, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ # buf = VFS_PAGE_SIZE;
used for: ls, s, lss, ss;
pre-writepage : ⊦ pre-writepage(inode, n, buf, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ # buf = VFS_PAGE_SIZE;
used for: ls, s, lss, ss;
pre-evict : ⊦ pre-evict(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files) ∧ inode.ino ≠ ROOT_INO;
used for: ls, s, lss, ss;
pre-readdir : ⊦ pre-readdir(ino, dirs, files) ↔ valid-dir-ino(ino, dirs, files);
used for: ls, s;
pre-truncate
: ⊦ pre-truncate(inode, n, pageno, buf-opt, dirs, files)
↔ valid-file-inode(inode, dirs, files) ∧ pageno = inode.size / VFS_PAGE_SIZE ∧ (buf-opt.some? → # buf-opt.buf = VFS_PAGE_SIZE);
used for: ls, s, lss, ss;
pre-iget : ⊦ pre-iget(ino, dirs, files) ↔ valid-ino(ino, dirs, files);
used for: ls, s;
pre-write-inode : ⊦ pre-write-inode(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files);
used for: ls, s, lss, ss;
valid-wb-inode : ⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files);
used for: ls, s;
valid-dir-inode
: ⊦ valid-dir-inode(inode, dirs, files)
↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size
∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory;
used for: ls, s;
valid-file-inode
: ⊦ valid-file-inode(inode, dirs, files)
↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory;
used for: ls, s;
end enrich