[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,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

nat-basic/a is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, inv-rmdir, inv-unlink,
nat-basic/c is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, inv-rmdir, inv-unlink,
nat-basic/f is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat-basic/l-01 is used by fsync-pages-inv,
nat-basic/l-05 is used by fsync-pages-inv,
nat-basic/lf is used by fsync-pages-inv,
nat-basic/lf-01 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-basic/lf-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-basic/ls-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-basic/oz is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
nat-basic/ref is used by fsync-pages-inv,
nat-basic/succ is used by fsync-pages-inv,
nat-basic/trans is used by fsync-pages-inv,

Used from specification abstract-file

abstract-file/elim is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsync, inv-write_inode, inv-truncate, inv-evict, inv-writepage, inv-readpage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
abstract-file/inj is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsync, inv-write_inode, inv-writepage, inv-readpage, inv-link, inv-unlink, inv-create,
abstract-file/sel-01 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, inv-write_inode, inv-evict, inv-writepage, inv-readpage, inv-rmdir, inv-mkdir,
abstract-file/sel-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsync, inv-truncate, inv-writepage, inv-renam, inv-link, inv-unlink, inv-create,
abstract-file/sel-06 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-writepage, inv-link, inv-unlink, inv-create,
abstract-file/sel-07 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-writepage, inv-link, inv-unlink, inv-create,
abstract-file/upd-04 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-unlink,
abstract-file/upd-05 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
abstract-file/upd-06 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-unlink,
abstract-file/upd-07 is used by inv-rename-file-dentry, inv-link, inv-unlink,
abstract-file/updsel-01 is used by inv-write_inode,
abstract-file/updsel-07 is used by inv-write_inode,
abstract-file/updsel-08 is used by fsync-pages-inv,
abstract-file/updsel-09 is used by inv-write_inode,
abstract-file/updsel-12 is used by fsync-inode-inv, inv-write_inode,
abstract-file/updsel-13 is used by fsync-inode-inv, inv-write_inode,

Used from specification afs-base

afs-base/afs-cons is used by inv-recover,
afs-base/at-upto is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
afs-base/orphans is used by inv-recover,
afs-base/afs-cons-dir-nlink is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup, inv-recover,
afs-base/afs-cons-file-nlink is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsync, inv-write_inode, inv-truncate, inv-evict, inv-writepage, inv-readpage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
afs-base/afs-cons-in-next is used by inv-rename-file-dentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, inv-evict, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
afs-base/afs-cons-init is used by inv-format,
afs-base/afs-cons-links-empty is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-evict, inv-mkdir,
afs-base/afs-cons-links-rmorphans is used by inv-recover,
afs-base/afs-cons-nlink0-notin is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
afs-base/afs-cons-non0 is used by inv-mkdir,
afs-base/afs-cons-notfile is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
afs-base/afs-cons-pagesize is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-writepage, inv-readpage, inv-link, inv-unlink, inv-create, inv-recover,
afs-base/afs-cons-root-dir is used by inv-evict, inv-recover,
afs-base/afs-cons-root-notfile is used by inv-rename-dentry, inv-evict,
afs-base/dir-empty is used by inv-rename-file-dentry, inv-rename-dir-dentry, inv-rename-dentry, inv-renam, inv-rmdir, inv-recover,
afs-base/getinode is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-write_inode, inv-evict, inv-writepage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-check-commit, inv-iget,
afs-base/in-upto is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
afs-base/links-add-entry is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-create,
afs-base/links-dec-nsubdirs is used by inv-rmdir,
afs-base/links-del-entry is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
afs-base/links-inc-nsubdirs is used by inv-rename-dir-negdentry,
afs-base/links-modmeta is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-unlink, inv-create,
afs-base/links-modmeta-write2 is used by inv-rename-file-negdentry, inv-rename-dir-dentry, inv-rmdir,
afs-base/links-modmeta-write3 is used by inv-rename-dir-dentry,
afs-base/links-nonempty is used by inv-rename-file-dentry, inv-rename-dir-dentry, inv-evict, inv-link, inv-rmdir, inv-unlink, inv-recover,
afs-base/root-not-orphan is used by inv-recover,
afs-base/subdirs-delete-orphans is used by inv-recover,
afs-base/valid-dentry-03 is used by inv-link,
afs-base/valid-dentry-with-parent is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
afs-base/valid-dir-ino is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-evict, inv-readdir, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
afs-base/valid-file-ino is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-write_inode, inv-truncate, inv-evict, inv-writepage, inv-readpage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-check-commit, inv-iget,
afs-base/valid-ino is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup, inv-check-commit, inv-recover, inv-iget,
afs-base/valid-inode is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-write_inode, inv-evict, inv-writepage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-check-commit, inv-iget,
afs-base/valid-negdentry is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-renam, inv-link, inv-mkdir, inv-create,
afs-base/valid-pagesize is used by inv-recover,
afs-base/valid-parent-ino is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,

Used from specification pcache-entry

Used from specification cache-base

Used from specification key

key/elim-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-link, inv-unlink, inv-create,
key/elim-03 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-evict, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
key/inj-01 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-link,
key/inj-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage, inv-readpage,
key/sel-01 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-mkdir, inv-create, inv-lookup,
key/sel-02 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create, inv-lookup,
key/sel-03 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-evict, inv-writepage, inv-readpage, inv-mkdir, inv-create,
key/sel-05 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage, inv-readpage,
key/test-01 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-evict, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
key/test-09 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-readpage, inv-link, inv-mkdir, inv-unlink, inv-create,

Used from specification min-max

min-max/min-comm is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
min-max/min-le-left is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,

Used from specification nat

nat/cancel-01 is used by fsync-pages-inv,
nat/elim-pred-c is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
nat/elim-sub is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/eq-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/fle is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/ge is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
nat/le is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat/le-def is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat/le-ls-simp is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/lels is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat/lels-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/lels-03 is used by fsync-pages-inv,
nat/lep is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
nat/lep-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat/ler is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat/ls is used by fsync-pages-inv,
nat/ls-01 is used by fsync-pages-inv,
nat/not-zero is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
nat/prop-07 is used by fsync-pages-inv,
nat/succ-01 is used by fsync-pages-inv,
nat/zero-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,

Used from specification store

store/dir-entries/At-other is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry,
store/file-content/At-other is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
store/icache/In-insert is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
store/dir-entries/At-in-out is used by inv-rename-file-negdentry, inv-rename-dir-negdentry, inv-link, inv-mkdir, inv-create,
store/dcache/At-in-out is used by inv-lookup,
store/icache/At-other is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
store/file-content/At-other is used by fsync-pages-inv,
store/dcache/At-other is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create,
store/pcache/At-other is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage, inv-readpage,
store/icache/At-same is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
store/dcache/At-same is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create, inv-lookup,
store/file-content/At-same is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
store/dir-entries/At-same is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create,
store/pcache/At-same is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage, inv-readpage,
store/dir-entries/Del-at is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry,
store/dcache/Del-at is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
store/icache/Del-at is used by inv-evict,
store/dir-entries/Del-at-strong is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
store/icache/Del-at-strong is used by inv-evict,
store/dir-entries/Del-empty is used by inv-rename-dir-dentry, inv-rmdir,
store/icache/Del-in is used by inv-evict,
store/dcache/Del-in is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
store/dir-entries/Del-in is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-unlink,
store/icache/In-empty is used by inv-format, inv-recover,
store/dcache/In-empty is used by inv-format, inv-recover,
store/dir-entries/In-empty is used by inv-rename-dir-dentry, inv-rmdir, inv-recover,
store/pcache/In-empty is used by inv-format, inv-recover,
store/file-content/In-insert is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
store/pcache/In-insert is used by inv-readpage,
store/dcache/In-insert is used by inv-link, inv-mkdir, inv-lookup,
store/icache/In-insert is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-unlink,
store/dir-entries/In-insert is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create,
store/dir-entries/Size-empty is used by inv-recover,
store/dcache/del-put is used by inv-rename-file-dentry, inv-rename-dir-dentry,
store/dir-entries/del-put is used by inv-rename-file-dentry, inv-rename-dir-dentry,
store/icache/in-neq is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
store/dcache/in-neq is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create, inv-lookup,
store/pcache/in-neq is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage, inv-readpage,
store/dir-entries/ins is used by inv-rename-file-dentry, inv-rename-dir-dentry,
store/icache/ins is used by fsync-inode-inv,
store/icache/insin is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
store/pcache/insin is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
store/dcache/insin is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-mkdir, inv-create,
store/file-content/insin is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv, inv-writepage,
store/dir-entries/insin is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-link, inv-mkdir, inv-create,
store/icache/insins is used by inv-rename-file-dentry, inv-rename-dir-dentry, inv-rmdir,
store/icache/k-At-same is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-unlink,
store/dcache/k-At-same is used by inv-mkdir,
store/pcache/notmemlookup is used by inv-truncate-buff-none-uncached,
store/icache/notmemlookup is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
store/dir-entries/notmemlookup is used by inv-rename-file-negdentry,

Used from specification error-class

error-class/ecommit is used by fsync-pages-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-check-commit,
error-class/efail is used by inv-format, inv-readdir, inv-readpage, inv-lookup, inv-recover, inv-iget,
error-class/esuccess is used by fsync-pages-inv, inv-format, inv-recover,
error-class/not-esuccess is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, fsync-inode-inv, inv-format, inv-write_inode, inv-writepage, inv-readpage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup, inv-recover, inv-iget,

Used from specification error

error/disj-33 is used by inv-lookup,
error/disj-91 is used by fsync-pages-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-check-commit,

Used from specification set-basic

set-basic/alink-set/Size-empty is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
set-basic/alink-set/ne is used by inv-rename-dir-negdentry, inv-rename-dir-dentry,
set-basic/alink-set/size-zero is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-evict, inv-mkdir, inv-unlink,
set-basic/alink-set/size-zero-01 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-evict, inv-mkdir,
set-basic/alink-set/size-zero-02 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-evict, inv-mkdir,

Used from specification dentry

dentry/disj is used by inv-rename-file-negdentry, inv-rename-dir-negdentry,
dentry/elim is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, inv-write_inode, inv-evict, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
dentry/elim-02 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-dir-negdentry, inv-renam, inv-link, inv-mkdir, inv-create,
dentry/inj is used by inv-rename-file-dentry, inv-rename-dir-dentry,
dentry/sel-03 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
dentry/sel-04 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
dentry/sel-05 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
dentry/test-01 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-dir-negdentry, inv-renam, inv-link, inv-mkdir, inv-create,
dentry/test-02 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, inv-write_inode, inv-evict, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
dentry/test-03 is used by inv-rename-file-dentry, inv-rename-dir-dentry,
dentry/test-04 is used by inv-rename-file-negdentry, inv-rename-dir-negdentry,

Used from specification page

page/page-size is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,

Used from specification buffer-option

buffer-option/ex-01 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
buffer-option/sel is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
buffer-option/test-01 is used by inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-truncate,
buffer-option/test-03 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-truncate,
buffer-option/test-04 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-truncate,

Used from specification abstract-dir

abstract-dir/elim is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup, inv-recover,
abstract-dir/inj is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup,
abstract-dir/sel-03 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
abstract-dir/sel-04 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
abstract-dir/sel-05 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-evict, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
abstract-dir/sel-08 is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-recover,
abstract-dir/sel-09 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-lookup, inv-recover,
abstract-dir/upd-03 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
abstract-dir/upd-04 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
abstract-dir/upd-05 is used by inv-rename-dir-dentry, inv-rmdir,
abstract-dir/upd-08 is used by inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/upd-09 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
abstract-dir/updsel-01 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/updsel-03 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/updsel-09 is used by inv-rename-file-dentry, inv-rename-dir-dentry,
abstract-dir/updsel-11 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/updsel-13 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-rmdir, inv-unlink,
abstract-dir/updsel-20 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/updsel-21 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,
abstract-dir/updsel-24 is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir, inv-mkdir,

Used from specification pcache-del-ops

pcache-del-ops/at-truncate is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
pcache-del-ops/in-evict-other is used by inv-evict,
pcache-del-ops/at-evict-other is used by inv-evict,
pcache-del-ops/in-truncate is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,

Used from specification array-copy

array-copy/buffer/size-fill-h is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,

Used from specification nat-mult

nat-mult/coef-18 is used by fsync-pages-inv,
nat-mult/mult-a is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat-mult/mult-c is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, fsync-pages-inv,
nat-mult/rsucc-02 is used by fsync-pages-inv,
nat-mult/zero-01 is used by fsync-pages-inv,

Used from specification icache-entry

icache-entry/elim is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage, inv-readpage, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
icache-entry/inj is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-iget,
icache-entry/sel-01 is used by fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage,
icache-entry/sel-02 is used by fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-evict, inv-writepage,
icache-entry/upd-02 is used by fsync-inode-inv,

Used from specification heap

heap/file-heap/at-alloc is used by inv-create,
heap/dir-heap/at-alloc is used by inv-mkdir,
heap/dir-heap/at-del is used by inv-evict,
heap/file-heap/at-del is used by inv-evict,
heap/file-heap/at-diffs is used by inv-recover,
heap/dir-heap/at-diffs is used by inv-recover,
heap/dir-heap/at-write is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
heap/file-heap/at-write is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-writepage, inv-link, inv-rmdir, inv-unlink, inv-create,
heap/dir-heap/in-alloc is used by inv-mkdir,
heap/file-heap/in-alloc is used by inv-create,
heap/file-heap/in-del is used by inv-evict,
heap/dir-heap/in-del is used by inv-evict,
heap/file-heap/in-diffs is used by inv-recover,
heap/dir-heap/in-diffs is used by inv-recover,
heap/file-heap/in-write is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-dentry, fsync-pages-inv, fsync-inode-inv, inv-write_inode, inv-writepage, inv-link, inv-unlink, inv-create,
heap/dir-heap/in-write is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-write_inode, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
heap/dir-heap/nonnull is used by inv-mkdir,
heap/dir-heap/overwrite is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
heap/file-heap/overwrite is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, fsync-inode-inv, inv-write_inode, inv-link, inv-rmdir, inv-unlink,
heap/dir-heap/overwrite-split is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rmdir,
heap/dir-heap/overwrite-split2 is used by inv-rename-dir-dentry,
heap/dir-heap/write-again is used by inv-rename-file-dentry, inv-rename-dir-dentry,

Used from specification afs-pre

afs-pre/pre-create is used by inv-create,
afs-pre/pre-evict is used by inv-evict,
afs-pre/pre-iget is used by inv-iget,
afs-pre/pre-link is used by inv-link,
afs-pre/pre-lookup is used by inv-lookup,
afs-pre/pre-mkdir is used by inv-mkdir,
afs-pre/pre-readdir is used by inv-readdir,
afs-pre/pre-readpage is used by inv-readpage,
afs-pre/pre-rename is used by inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-renam,
afs-pre/pre-rmdir is used by inv-rmdir,
afs-pre/pre-truncate is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-truncate,
afs-pre/pre-unlink is used by inv-unlink,
afs-pre/pre-write-inode is used by fsync-inode-inv, inv-write_inode,
afs-pre/pre-writepage is used by fsync-pages-inv, inv-writepage,
afs-pre/valid-dir-inode is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-evict, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create,
afs-pre/valid-file-inode is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-pages-inv, fsync-inode-inv, inv-fsyncdir, inv-fsync, inv-sync, inv-write_inode, inv-truncate, inv-evict, inv-writepage, inv-renam, inv-link, inv-rmdir, inv-mkdir, inv-unlink, inv-create, inv-check-commit, inv-iget,
afs-pre/valid-wb-inode is used by inv-rename-negdentry, inv-rename-file-negdentry, inv-rename-file-dentry, inv-rename-dir-negdentry, inv-rename-dir-dentry, inv-rename-dentry, fsync-inode-inv, inv-write_inode, inv-evict, inv-renam,

Used from specification inode

Used from specification nat-div

nat-div/rax is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-div/cond is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-div/cond-01 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
nat-div/mod-le-02 is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,

Used from specification afs-asm

afs-asm/afs-cons-rename-dir-dentry is used by inv-rename-dir-dentry,
afs-asm/afs-cons-rename-dir-negdentry is used by inv-rename-dir-negdentry,
afs-asm/afs-cons-rename-file-dentry is used by inv-rename-file-dentry,
afs-asm/afs-cons-rename-file-negdentry is used by inv-rename-file-negdentry,
afs-asm/inv-create is used by inv-create,
afs-asm/inv-evict is used by inv-evict,
afs-asm/inv-link is used by inv-link,
afs-asm/inv-mkdir is used by inv-mkdir,
afs-asm/inv-rmdir is used by inv-rmdir,
afs-asm/inv-truncate is used by inv-truncate-buff-some, inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached,
afs-asm/inv-unlink is used by inv-unlink,
afs-asm/inv-write_inode is used by fsync-inode-inv, inv-write_inode,
afs-asm/inv-writepage is used by fsync-pages-inv, inv-writepage,

Used from specification pcache-asm

pcache-asm/inv-evict is used by inv-evict,