[CBMC] Add assert with readability check

test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c

@@ -37,8 +37,9 @@
 
 #include "../../utility/memory_assignments.c"
 
-/* This proof assumes that pxDuplicateNetworkBufferWithDescriptor is implemented correctly. */
+#include "cbmc.h"
 
+/* This proof assumes that pxDuplicateNetworkBufferWithDescriptor is implemented correctly. */
 void publicTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
                             NetworkBufferDescriptor_t * pxNetworkBuffer,
                             uint32_t ulLen,
@@ -59,12 +60,23 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ
     return pxNetworkBuffer;
 }
 
+BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * pxDescriptor,
+                                    BaseType_t xReleaseAfterSend )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assert( pxDescriptor != NULL , "The descriptor cannot be NULL" );
+    __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL" );
+
+    return xReturn;
+}
+
 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
                                      size_t uxBufferLength,
                                      BaseType_t xOutgoingPacket )
 {
     __CPROVER_assert( pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL" );
-    __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength );
+    __CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "pucEthernetBuffer should be readable." );
 
     uint16_t usReturn;
     return usReturn;
@@ -75,7 +87,7 @@ uint16_t usGenerateChecksum( uint16_t usSum,
                              size_t uxByteCount )
 {
     __CPROVER_assert( pucNextData != NULL, "The next data pointer cannot be NULL" );
-    __CPROVER_r_ok( pucNextData, uxByteCount );
+    __CPROVER_assert( __CPROVER_r_ok( pucNextData, uxByteCount ), "The pucNextData should be readable." );
 
     uint16_t usReturn;
     return usReturn;
@@ -86,16 +98,30 @@ void harness()
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
     NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
 
+    /* The code does not expect both of these to be equal to NULL at the same time. */
+    __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL );
+
+    uint32_t ulLen;
+
+    /* If network buffer is properly created. */
     if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) )
     {
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
+        /* Assume that the length is proper. */
+        __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen + ipSIZE_OF_ETH_HEADER );
         __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
     }
+    /* If not. */
+    else
+    {
+        /* Assume that the length is proper. The length should be between this range. It
+         * is made so by the functions up the call tree. Essentially, this is equal to a
+         * TCP packet header with and without TCP options. */
+        __CPROVER_assume( ( ulLen >= ipSIZE_OF_IPv4_HEADER + ipSIZE_OF_TCP_HEADER ) &&
+                          ( ulLen <= ipSIZE_OF_IPv4_HEADER + ipSIZE_OF_TCP_HEADER + 40 /* Maximum option bytes. */ ) );
+    }
 
-    uint32_t ulLen;
     BaseType_t xReleaseAfterSend;
 
-    /* The code does not expect both of these to be equal to NULL at the same time. */
-    __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL );
     publicTCPReturnPacket( pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend );
 }