1 files changed, 100 insertions, 0 deletions
diff --git a/FreeRTOS/Test/CBMC/include/cbmc.h b/FreeRTOS/Test/CBMC/include/cbmc.h
new file mode 100644
index 000000000..c30063bae
--- /dev/null
+++ b/FreeRTOS/Test/CBMC/include/cbmc.h
@@ -0,0 +1,100 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.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 "FreeRTOS_DHCP.h"
+#include "NetworkBufferManagement.h"
+#include "NetworkInterface.h"
+
+/*
+  * CBMC models a pointer as an object id and an offset into that
+  * object.  The top bits of a pointer encode the object id and the
+  * remaining bits encode the offset.  This means there is a bound on
+  * the maximum offset into an object in CBMC, and hence a bound on the
+  * size of objects in CBMC.
+  */
+#define CBMC_BITS               7
+#define CBMC_MAX_OBJECT_SIZE    ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) )
+
+#define IMPLIES( a, b )    ( !( a ) || ( b ) )
+
+BaseType_t nondet_basetype();
+UBaseType_t nondet_ubasetype();
+TickType_t nondet_ticktype();
+int32_t nondet_int32();
+uint32_t nondet_uint32();
+size_t nondet_sizet();
+
+#define nondet_BaseType()    nondet_basetype()
+
+void * safeMalloc( size_t size );
+
+
+enum CBMC_LOOP_CONDITION
+{
+    CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN
+};
+
+/* CBMC specification: capture old value for precondition and */
+/* postcondition checking */
+
+#define OLDVAL( var )              _old_ ## var
+#define SAVE_OLDVAL( var, typ )    const typ OLDVAL( var ) = var
+
+/* CBMC specification: capture old value for values passed by */
+/* reference in function abstractions */
+
+#define OBJ( var )                 ( * var )
+#define OLDOBJ( var )              _oldobj_ ## var
+#define SAVE_OLDOBJ( var, typ )    const typ OLDOBJ( var ) = OBJ( var )
+
+/* CBMC debugging: printfs for expressions */
+
+#define __CPROVER_printf( var )          { uint32_t ValueOf_ ## var = ( uint32_t ) var; }
+#define __CPROVER_printf2( str, exp )    { uint32_t ValueOf_ ## str = ( uint32_t ) ( exp ); }
+
+/* CBMC debugging: printfs for pointer expressions */
+
+#define __CPROVER_printf_ptr( var )          { uint8_t * ValueOf_ ## var = ( uint8_t * ) var; }
+#define __CPROVER_printf2_ptr( str, exp )    { uint8_t * ValueOf_ ## str = ( uint8_t * ) ( exp ); }
+
+/*
+  * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes.
+  * This assertion is used in some of the TaskPool proofs.
+  */
+#define __CPROVER_assert_zero_allocation()       \
+    __CPROVER_assert( pvPortMalloc( 0 ) == NULL, \
+                      "pvPortMalloc allows zero-allocated memory." )
+
+/*
+  * A stub for pvPortMalloc that nondeterministically chooses to return
+  * either NULL or an allocation of the requested space.  The stub is
+  * guaranteed to return NULL when asked to allocate 0 bytes.
+  * This stub is used in some of the TaskPool proofs.
+  */
+void * pvPortMalloc( size_t xWantedSize )
+{
+    if( xWantedSize == 0 )
+    {
+        return NULL;
+    }
+
+    return nondet_bool() ? malloc( xWantedSize ) : NULL;
+}
+
+void vPortFree( void * pv )
+{
+    ( void ) pv;
+    free( pv );
+}