Fix DNSHandlePacket CBMC test

FreeRTOS · Jul 11, 2024 · 6a7eff0 · 6a7eff0
1 parent 598d87a
commit 6a7eff0
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 5 deletions.
diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
@@ -7,11 +7,18 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
-/* Function prvParseDNSReply is proven to be correct separately. */
-uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                           size_t xBufferLength,
-                           BaseType_t xExpected )
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Function DNS_ParseDNSReply is proven to be correct separately. */
+uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                            size_t uxBufferLength,
+                            struct freertos_addrinfo ** ppxAddressInfo,
+                            BaseType_t xExpected,
+                            uint16_t usPort )
 {
+    __CPROVER_assert( pucUDPPayloadBuffer != NULL, "pucUDPPayloadBuffer cannot be NULL" );
+    return nondet_uint32();
 }
 
 void harness()

diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json
@@ -4,7 +4,8 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
   ],
   "DEF":
   [