1 /* Standard includes. */ 2 #include <stdint.h> 3 #include <stdio.h> 4 5 /* FreeRTOS includes. */ 6 #include "FreeRTOS.h" 7 #include "task.h" 8 #include "semphr.h" 9 10 /* FreeRTOS+TCP includes. */ 11 #include "FreeRTOS_IP.h" 12 #include "FreeRTOS_Sockets.h" 13 #include "FreeRTOS_IP_Private.h" 14 #include "FreeRTOS_UDP_IP.h" 15 #include "FreeRTOS_DNS.h" 16 #include "FreeRTOS_DHCP.h" 17 #include "NetworkBufferManagement.h" 18 #include "NetworkInterface.h" 19 20 /* 21 * CBMC models a pointer as an object id and an offset into that 22 * object. The top bits of a pointer encode the object id and the 23 * remaining bits encode the offset. This means there is a bound on 24 * the maximum offset into an object in CBMC, and hence a bound on the 25 * size of objects in CBMC. 26 */ 27 #define CBMC_BITS 7 28 #define CBMC_MAX_OBJECT_SIZE ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) ) 29 30 #define IMPLIES( a, b ) ( !( a ) || ( b ) ) 31 32 BaseType_t nondet_basetype(); 33 UBaseType_t nondet_ubasetype(); 34 TickType_t nondet_ticktype(); 35 int32_t nondet_int32(); 36 uint32_t nondet_uint32(); 37 size_t nondet_sizet(); 38 39 #define nondet_BaseType() nondet_basetype() 40 41 void * safeMalloc( size_t size ); 42 43 44 enum CBMC_LOOP_CONDITION 45 { 46 CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN 47 }; 48 49 /* CBMC specification: capture old value for precondition and */ 50 /* postcondition checking */ 51 52 #define OLDVAL( var ) _old_ ## var 53 #define SAVE_OLDVAL( var, typ ) const typ OLDVAL( var ) = var 54 55 /* CBMC specification: capture old value for values passed by */ 56 /* reference in function abstractions */ 57 58 #define OBJ( var ) ( * var ) 59 #define OLDOBJ( var ) _oldobj_ ## var 60 #define SAVE_OLDOBJ( var, typ ) const typ OLDOBJ( var ) = OBJ( var ) 61 62 /* CBMC debugging: printfs for expressions */ 63 64 #define __CPROVER_printf( var ) { uint32_t ValueOf_ ## var = ( uint32_t ) var; } 65 #define __CPROVER_printf2( str, exp ) { uint32_t ValueOf_ ## str = ( uint32_t ) ( exp ); } 66 67 /* CBMC debugging: printfs for pointer expressions */ 68 69 #define __CPROVER_printf_ptr( var ) { uint8_t * ValueOf_ ## var = ( uint8_t * ) var; } 70 #define __CPROVER_printf2_ptr( str, exp ) { uint8_t * ValueOf_ ## str = ( uint8_t * ) ( exp ); } 71 72 /* 73 * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes. 74 * This assertion is used in some of the TaskPool proofs. 75 */ 76 #define __CPROVER_assert_zero_allocation() \ 77 __CPROVER_assert( pvPortMalloc( 0 ) == NULL, \ 78 "pvPortMalloc allows zero-allocated memory." ) 79 80 /* 81 * A stub for pvPortMalloc that nondeterministically chooses to return 82 * either NULL or an allocation of the requested space. The stub is 83 * guaranteed to return NULL when asked to allocate 0 bytes. 84 * This stub is used in some of the TaskPool proofs. 85 */ pvPortMalloc(size_t xWantedSize)86void * pvPortMalloc( size_t xWantedSize ) 87 { 88 if( xWantedSize == 0 ) 89 { 90 return NULL; 91 } 92 93 return nondet_bool() ? malloc( xWantedSize ) : NULL; 94 } 95 vPortFree(void * pv)96void vPortFree( void * pv ) 97 { 98 ( void ) pv; 99 free( pv ); 100 } 101
