Safety Property: LimitFilePath

property LimitFilePath (path: String) {
    requires AbsoluteFileNames;
    
    check RFile.RFile (pathname: String) {
        String aname;
        aname = getAbsoluteName ();
        
        if (!aname.startsWith (path)) {
            violation ("Attempt to access illegal file " + aname +
                       ".  Only files in the subtree " + path + 
                       " may be accessed.");
        }
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science