Safety Property: NetConnectionMaxSendAmount

property NetConnectionMaxSendAmount (maxBytes: int) {
  // Limit total data sent through each connection.
  requires IndividualNetworkByteCount;
  check RNetConnection.preSend (nbytes: int) {
    if (bytesSent + nbytes > maxBytes) {
      violation 
        ("Maximum per-connection send data amount exceeded for connection " +
         toString () + ". Maximum of " + maxBytes + 
         " bytes per connection. Already sent " + bytesSent + 
         " bytes; attempting to send " + nbytes + 
         " bytes.");
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science