Safety Property: LimitObserveFiles

property LimitObserveFiles (n: int) {
  requires FileObservationCountFileNames;
  check RFileSystem.observeProperty (file: RFile) {
    if (nobservations > n) {
      violation ("File snooping limit (" + n + 
                 ") exceeded.  Trying to observe: " + file.getName ());
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science