1 files changed, 130 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c
new file mode 100644
index 000000000..3ae1256a0
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c
@@ -0,0 +1,130 @@
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "queue.h"
+#include "list.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_DNS.h"
+#include "NetworkBufferManagement.h"
+#include "NetworkInterface.h"
+#include "IPTraceMacroDefaults.h"
+
+#include "cbmc.h"
+
+/****************************************************************
+ * Signature of function under test
+ ****************************************************************/
+
+uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
+			   size_t uxBufferLength,
+			   BaseType_t xExpected );
+
+/****************************************************************
+ * Abstraction of prvReadNameField proved in ReadNameField
+ ****************************************************************/
+
+size_t prvReadNameField( const uint8_t *pucByte,
+			 size_t uxRemainingBytes,
+			 char *pcName,
+			 size_t uxDestLen )
+{
+  __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
+		   "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
+  __CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE,
+		   "NAME_SIZE < CBMC_MAX_OBJECT_SIZE");
+  __CPROVER_assert(NAME_SIZE >= 4,
+		   "NAME_SIZE >= 4 required for good coverage.");
+
+
+  /* Preconditions */
+  __CPROVER_assert(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE,
+		   "ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)");
+  __CPROVER_assert(uxDestLen < CBMC_MAX_OBJECT_SIZE,
+		   "ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)");
+
+  __CPROVER_assert(uxRemainingBytes <= NETWORK_BUFFER_SIZE,
+		   "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)");
+
+  /* This precondition in the function contract for prvReadNameField
+   * fails because prvCheckOptions called prvReadNameField with the
+   * constant value 254.
+  __CPROVER_assert(uxDestLen <= NAME_SIZE,
+		   "ReadNameField: uxDestLen <= NAME_SIZE)");
+  */
+
+  __CPROVER_assert( pucByte != NULL ,
+		    "ReadNameField:  pucByte != NULL )");
+  __CPROVER_assert( pcName != NULL ,
+		    "ReadNameField:  pcName != NULL )");
+
+  __CPROVER_assert(uxDestLen > 0,
+		   "ReadNameField: uxDestLen > 0)");
+
+  /* Return value */
+  size_t index;
+
+  /* Postconditions */
+  __CPROVER_assume( index <= uxDestLen+1 && index <= uxRemainingBytes );
+
+  return index;
+}
+
+/****************************************************************
+ * Abstraction of prvSkipNameField proved in SkipNameField
+ ****************************************************************/
+
+size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength )
+{
+
+  __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
+		   "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
+
+
+  /* Preconditions */
+  __CPROVER_assert(uxLength < CBMC_MAX_OBJECT_SIZE,
+		   "SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)");
+  __CPROVER_assert(uxLength <= NETWORK_BUFFER_SIZE,
+		   "SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)");
+  __CPROVER_assert(pucByte != NULL,
+		   "SkipNameField: pucByte != NULL)");
+
+  /* Return value */
+  size_t index;
+
+  /* Postconditions */
+  __CPROVER_assume(index <= uxLength);
+
+  return index;
+}
+
+/****************************************************************
+ * Proof of prvParseDNSReply
+ ****************************************************************/
+
+void harness() {
+
+  size_t uxBufferLength;
+  BaseType_t xExpected;
+  uint8_t *pucUDPPayloadBuffer = malloc(uxBufferLength);
+
+  __CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
+		   "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
+
+  __CPROVER_assume(uxBufferLength < CBMC_MAX_OBJECT_SIZE);
+  __CPROVER_assume(uxBufferLength <= NETWORK_BUFFER_SIZE);
+  __CPROVER_assume(pucUDPPayloadBuffer != NULL);
+
+  uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer,
+				     uxBufferLength,
+				     xExpected );
+
+}