Safety Property: NetMaxSendAmount

property NetMaxSendAmount (maxBytes: int) {
  // Limit total data sent over the network.
  requires GlobalNetworkByteCount;

  check RNetwork.preSend (remote: RNetAddress, nbytes: int) {
    if (gBytesSent + nbytes > maxBytes) {
        violation 
            ("Maximum network send limit exceeded.  Maximum of " +
             maxBytes + " bytes. Already send " + gBytesSent + 
             "; attempting to send " +  nbytes + " bytes.");
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science