1 files changed, 102 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c
new file mode 100644
index 000000000..86e30b1fd
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c
@@ -0,0 +1,102 @@
+/* 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
+ ****************************************************************/
+
+size_t prvReadNameField( const uint8_t *pucByte,
+			 size_t uxRemainingBytes,
+			 char *pcName,
+			 size_t uxDestLen );
+
+/****************************************************************
+ * The function under test is not defined in all configurations
+ ****************************************************************/
+
+#if ( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )  
+
+/* prvReadNameField is defined in this configuration */
+
+#else
+
+/* prvReadNameField is not defined in this configuration, stub it. */
+
+size_t prvReadNameField( const uint8_t *pucByte,
+			 size_t uxRemainingBytes,
+			 char *pcName,
+			 size_t uxDestLen )
+{
+  return 0;
+}
+
+#endif
+
+
+/****************************************************************
+ * Proof of prvReadNameField function contract
+ ****************************************************************/
+
+void harness() {
+
+  __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.");
+
+
+  size_t uxRemainingBytes;
+  size_t uxDestLen;
+
+  uint8_t *pucByte = malloc(uxRemainingBytes);
+  char *pcName = malloc(uxDestLen);
+
+  /* Preconditions */
+
+  __CPROVER_assume(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE);
+  __CPROVER_assume(uxDestLen < CBMC_MAX_OBJECT_SIZE);
+
+  __CPROVER_assume(uxRemainingBytes <= NETWORK_BUFFER_SIZE);
+  __CPROVER_assume(uxDestLen <= NAME_SIZE);
+
+  __CPROVER_assume( pucByte != NULL );
+  __CPROVER_assume( pcName != NULL );
+
+  /* Avoid overflow on uxSourceLen - 1U with uxSourceLen == uxRemainingBytes */
+  //__CPROVER_assume(uxRemainingBytes > 0);
+
+  /* Avoid overflow on uxDestLen - 1U */
+  __CPROVER_assume(uxDestLen > 0);
+
+  size_t index = prvReadNameField( pucByte,
+				   uxRemainingBytes,
+				   pcName,
+				   uxDestLen );
+
+  /* Postconditions */
+
+  __CPROVER_assert( index <= uxDestLen+1 && index <= uxRemainingBytes,
+		    "prvReadNamefield: index <= uxDestLen+1");
+}