property TarLimitReadWrite {
requires TrackTotalBytesRead, TrackTotalBytesWritten;
check RFileSystem.preWrite (file: RFile, n: int) {
if (RFileSystem.bytes_written + n
> ((RFileSystem.bytes_read * 2) + 12000)) {
violation
("Write limit exceeded. Should not be more than 2 * read + 12000. " +
"Read: " + RFileSystem.bytes_read + ", attempting to write " +
n + ", already written " + RFileSystem.bytes_written + ".");
}
}
}
Naccio Home Page
University of Virginia, Computer Science