blob: c30063bae346f25874ea99aad058005e0ca71320 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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 );
}
|
