Safety Property: FileAccess



property FileAccess {
    requires AbsoluteFileNames;

    check RFileSystem.openRead (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkRead (file.getAbsoluteName ());
        }
    }
 
    check RFileSystem.openOverwrite (file: RFile),
        RFileSystem.openCreate (file: RFile),
        RFileSystem.openAppend (file: RFile) {
        SecurityManager security = getSecurityManager ();
        if (security != null) {
            security.checkWrite (file.getAbsoluteName ());
        }
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science