You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
101 lines
2.9 KiB
C
101 lines
2.9 KiB
C
/* 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 );
|
|
}
|