Safety Property: FileObservations



property FileObservations {
    check RFileSystem.observeExists (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkRead (file.getAbsoluteName ());
        }
    }

    check RFileSystem.observeWriteable (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkWrite (file.getAbsoluteName ());
        }
    }

    check RFileSystem.observeReadable (file: RFile),
        RFileSystem.observeIsFile (file: RFile),
        RFileSystem.observeLastModifiedTime (file: RFile),
        RFileSystem.observeLength (file: RFile),
        RFileSystem.observeList (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkRead (file.getAbsoluteName ());
        }
    }

    check RFileSystem.preDelete (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkDelete (file.getAbsoluteName ());
            // reveals if its a directory
            security.checkRead (file.getAbsoluteName ());
        }
    }

    check RFileSystem.makeDirectory (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkWrite (file.getAbsoluteName ());
        }
    }

    check RFileSystem.renameReplace (file: RFile, newfile: RFile),
        RFileSystem.renameNew (file: RFile, newfile: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            // Yes, it really doesn't call checkRead!  I think it should...
            security.checkWrite (file.getAbsoluteName ());
            security.checkWrite (newfile.getAbsoluteName ());
        }
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science