| vfs_rename#(PATH, PATH', USER, OF; ERR, DIRS, FILES, ASYNCED) {choose OLD_DENT, NEW_DENT, ISDIR, INODE, OLD_INODE, NEW_INODE, DEL_INODE, OLD_DENT_INODE, NEW_DENT_INODE with true in if PATH = ε ∨ PATH' = ε ∨ PATH ⊑ PATH' then ERR := EACCESS else {let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH) in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then let ISRENAME = true in vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DEL_INODE, ISDIR, ERR); OLD_INODE := INODE; OLD_DENT := DENT; OLD_DENT_INODE := DEL_INODE}; if ERR = ESUCCESS then let INO = ROOT_INO, DENT = negdentry(PATH'.last), PATH = parent(PATH') in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ENOENT then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR) else if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR)}; NEW_INODE := INODE; NEW_DENT := DENT; NEW_DENT_INODE := DEL_INODE}; if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then let DENT = NEW_DENT in {afs_rename#(; OLD_INODE, NEW_INODE, OLD_DENT_INODE, NEW_DENT_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED); if DENT.dentry? then vfs_put_inode#(NEW_DENT_INODE, OF, ASYNCED; ERR, DIRS, FILES)}} } |