Safety Property: NetMaxReceiveAmount

property NetMaxReceiveAmount (maxBytes: int) {
  // Limit total data received from network.
  requires GlobalNetworkByteCount;
  check RNetwork.preReceive (remote: RNetAddress, nbytes: int) {
    if (gBytesReceived + nbytes > maxBytes) {
      if (gBytesReceived == 0) {
        violation 
          ("Maximum network receive data amount exceeded.  Maximum of " +
           maxBytes + " bytes; about to receive " + 
           nbytes + " bytes."); 
      } else {
        violation
          ("Maximum network receive data amount exceeded.  Maximum of " +
           maxBytes + " bytes.  " + gBytesReceived +
           " already received; about to receive " + 
           nbytes + " bytes.");
      }
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science