// Note: int/int switch hack!
property LimitBytesWritten (limit: int) {
requires TrackTotalBytesWritten, FileNames;
check RFileSystem.preWrite (file: RFile, n: int) {
if (bytes_written + n > limit) {
violation ("Attempt to write more than " + limit +
" bytes. Already written " +
bytes_written + " bytes, writing " +
n + " more to " +
file.getName () + ".");
}
}
}
Naccio Home Page
University of Virginia, Computer Science