text: /* Standard includes. */
  #include <stdint.h>
  #include <stdio.h>
  
  /* FreeRTOS includes. */
  #include "FreeRTOS.h"
  #include "task.h"
  #include "queue.h"
  #include "semphr.h"
  
  /* FreeRTOS+TCP includes. */
  #include "FreeRTOS_IP.h"
  #include "FreeRTOS_Sockets.h"
  #include "FreeRTOS_IP_Private.h"
  #include "FreeRTOS_UDP_IP.h"
  #include "FreeRTOS_TCP_IP.h"
  #include "FreeRTOS_DHCP.h"
  #include "NetworkInterface.h"
  #include "NetworkBufferManagement.h"
  #include "FreeRTOS_ARP.h"
  #include "FreeRTOS_TCP_WIN.h"
  
  #include "cbmc.h"
  
  void prvCheckOptions( FreeRTOS_Socket_t *pxSocket,
  		      NetworkBufferDescriptor_t *pxNetworkBuffer );
  
  // Used in specification and abstraction of CheckOptions inner and outer loops
  // Given unconstrained values in harness
  size_t buffer_size;
  uint8_t *EthernetBuffer;
  
  // Abstraction of CheckOptions outer loop used in proof of CheckOptions
  // Loop variables passed by reference: VAL(var) is (*var).
  BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr,
  					  const unsigned char ** const ppucLast,
  					  FreeRTOS_Socket_t ** const ppxSocket,
  					  TCPWindow_t ** const ppxTCPWindow)
  {
    // CBMC pointer model (obviously true)
    __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE);
  
    // Preconditions
  
    // pucPtr is a valid pointer
    __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) &&
  		   OBJ(ppucPtr) < EthernetBuffer + buffer_size,
  		   "pucPtr is a valid pointer");
    // pucLast is a valid pointer (or one past)
    __CPROVER_assert(EthernetBuffer <= OBJ(ppucLast) &&
  		   OBJ(ppucLast) <= EthernetBuffer + buffer_size,
  		   "pucLast is a valid pointer");
    // pucPtr is before pucLast
    __CPROVER_assert(OBJ(ppucPtr) < OBJ(ppucLast),
  		   "pucPtr < pucLast");
  
    // Record initial values
    SAVE_OLDOBJ(ppucPtr, unsigned char *);
    SAVE_OLDOBJ(ppucLast, unsigned char *);
  
    // Model loop body
    size_t offset;
    BaseType_t rc;
    OBJ(ppucPtr) += offset;
  
    // Postconditions
  
    // rc is boolean
    __CPROVER_assume(rc == pdTRUE || rc == pdFALSE);
    // pucPtr advanced
    __CPROVER_assume(rc == pdFALSE || OLDOBJ(ppucPtr) < OBJ(ppucPtr));
    // pucLast unchanged
    __CPROVER_assume(OBJ(ppucLast) == OLDOBJ(ppucLast));
    // pucPtr <= pucLast
    __CPROVER_assume(OBJ(ppucPtr) <= OBJ(ppucLast));
  
    return rc;
  }
  
  // Proof of CheckOptions
  void harness()
  {
    // Buffer can be any buffer of size at most BUFFER_SIZE
    size_t offset;
    uint8_t buffer[BUFFER_SIZE];
    buffer_size = BUFFER_SIZE - offset;
    EthernetBuffer = buffer + offset;
  
    // pxSocket can be any socket
    FreeRTOS_Socket_t pxSocket;
  
    // pxNetworkBuffer can be any buffer descriptor with any buffer
    NetworkBufferDescriptor_t pxNetworkBuffer;
    pxNetworkBuffer.pucEthernetBuffer = EthernetBuffer;
    pxNetworkBuffer.xDataLength = buffer_size;
  
    ////////////////////////////////////////////////////////////////
    // Specification and proof of CheckOptions
  
    // CBMC pointer model (obviously true)
    __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE);
  
    // Buffer overflow on pathologically small buffers
    // Must be big enough to hold pxTCPPacket and pxTCPHeader
    __CPROVER_assume(buffer_size > 47);
  
    // EthernetBuffer is a valid pointer (or one past when buffer_size==0)
    __CPROVER_assume(buffer <= EthernetBuffer &&
  		   EthernetBuffer <= buffer + BUFFER_SIZE);
  
    // Loop variables passed by reference
    prvCheckOptions(&pxSocket, &pxNetworkBuffer);
  }
  