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"
  
  BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr,
  					  const unsigned char ** const ppucLast,
  					  FreeRTOS_Socket_t ** const ppxSocket,
  					  TCPWindow_t ** const ppxTCPWindow);
  
  // Given unconstrained values in harness
  size_t buffer_size;
  uint8_t *EthernetBuffer;
  
  void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr,
  				  FreeRTOS_Socket_t ** const ppxSocket,
  				  unsigned char * const pucLen )
  {
    // Preconditions
  
    // pucPtr is a valid pointer
    __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) &&
  		   OBJ(ppucPtr) < EthernetBuffer + buffer_size,
  		   "pucPtr is a valid pointer");
    // pucPtr + 8 is a valid pointer
    __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) + 8 &&
  		   OBJ(ppucPtr) + 8 <= EthernetBuffer + buffer_size,
  		   "pucPtr+8 is a valid pointer");
    // len >= 8
    __CPROVER_assert(OBJ(pucLen) >= 8, "len >= 8");
  
    // Record initial values
    SAVE_OLDOBJ(ppucPtr, unsigned char *);
    SAVE_OLDOBJ(pucLen, unsigned char);
  
    // Model loop body
    OBJ(ppucPtr) += 8;
    OBJ(pucLen) -= 8;
  
    // Postconditions
  
    __CPROVER_assume(OBJ(ppucPtr) == OLDOBJ(ppucPtr) + 8);
    __CPROVER_assume(OBJ(pucLen) == OLDOBJ(pucLen) - 8);
    __CPROVER_assume(EthernetBuffer <= OBJ(ppucPtr) &&
  		   OBJ(ppucPtr) <= EthernetBuffer + buffer_size);
  }
  
  // Proof of CheckOptions outer loop
  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;
  
    // pucPtr and pucLast can be any pointers into buffer
    size_t pucPtr_offset;
    size_t pucLast_offset;
    unsigned char *pucPtr = EthernetBuffer + pucPtr_offset;
    unsigned char *pucLast = EthernetBuffer + pucLast_offset;
  
    // uxNewMSS can by any byte
    UBaseType_t uxNewMSS;
  
    // pxSocket can be any socket
    FreeRTOS_Socket_t xSocket;
    FreeRTOS_Socket_t *pxSocket = &xSocket;
  
    // pxTCPWindow can be any window (points into socket)
    TCPWindow_t *pxTCPWindow = &xSocket.u.xTCP.xTCPWindow;
  
    ////////////////////////////////////////////////////////////////
    // Specification and proof of CheckOptions outer loop
  
    // CBMC pointer model (obviously true)
    __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE);
  
    // Preconditions
  
    // pucPtr is a valid pointer
    __CPROVER_assume(EthernetBuffer <= pucPtr &&
  		   pucPtr < EthernetBuffer + buffer_size);
    // pucLast is a valid pointer (or one past)
    __CPROVER_assume(EthernetBuffer <= pucLast &&
  		   pucLast <= EthernetBuffer + buffer_size);
    // pucPtr is before pucLast
    __CPROVER_assume(pucPtr < pucLast);
  
    // Record initial values
    SAVE_OLDVAL(pucPtr, uint8_t *);
    SAVE_OLDVAL(pucLast, uint8_t *);
  
    // Loop variables passed by reference
    // Return value describes loop exit: break or continue
    BaseType_t rc =
      prvSingleStepTCPHeaderOptions(&pucPtr, &pucLast, &pxSocket, &pxTCPWindow);
  
    // Postconditions
    __CPROVER_assert(rc == pdFALSE || OLDVAL(pucPtr) < pucPtr, "pucPtr advanced");
    __CPROVER_assert(pucLast == OLDVAL(pucLast), "pucLast unchanged");
    __CPROVER_assert(pucPtr <= pucLast, "pucPtr <= pucLast");
  
  }
  