Fix CBMC proofs

tony-josi-aws · Jan 9, 2024 · ffd7756 · ffd7756
1 parent 5a559a9
commit ffd7756
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 4 deletions.
diff --git a/test/cbmc/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h
@@ -121,9 +121,13 @@
  * set to 1 if a valid configuration cannot be obtained from a DHCP server for any
  * reason.  The static configuration used is that passed into the stack by the
  * FreeRTOS_IPInit() function call. */
-#define ipconfigUSE_DHCP                         1
+#ifndef ipconfigUSE_DHCP
+    #define ipconfigUSE_DHCP                         1
+#endif
 
-#define ipconfigDHCP_REGISTER_HOSTNAME           1
+#ifndef ipconfigDHCP_REGISTER_HOSTNAME
+    #define ipconfigDHCP_REGISTER_HOSTNAME           1
+#endif
 
 #define ipconfigDHCP_USES_UNICAST                1
 
@@ -230,11 +234,15 @@
  * lower value can save RAM, depending on the buffer management scheme used.  If
  * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must
  * be divisible by 8. */
-#define ipconfigNETWORK_MTU                1500U
+#ifndef ipconfigNETWORK_MTU
+    #define ipconfigNETWORK_MTU                1500U
+#endif
 
 /* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver.  DNS is used
  * through the FreeRTOS_gethostbyname() API function. */
-#define ipconfigUSE_DNS                    1
+#ifndef ipconfigUSE_DNS
+    #define ipconfigUSE_DNS                    1
+#endif
 
 /* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will
  * generate replies to incoming ICMP echo (ping) requests. */

diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
@@ -161,6 +161,7 @@ void harness()
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface->pfAddAllowedMAC == NULL );
 
     if( nondet_bool() )
     {

diff --git a/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c b/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c
@@ -81,6 +81,11 @@ void harness()
     NetworkInterface_t * pxInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
     uint32_t ulLen;
 
+    if( pxInterface != NULL )
+    {
+        __CPROVER_assume( pxInterface->pfAddAllowedMAC == NULL );
+    }
+
     /* The code does not expect pxNetworkBuffer to be NULL. */
     __CPROVER_assume( pxNetworkBuffer != NULL );