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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
/* Standard includes. */
#include <stdint.h>
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "task.h"
#include "queue.h"
#include "list.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 "NetworkBufferManagement.h"
#include "NetworkInterface.h"
#include "IPTraceMacroDefaults.h"
#include "cbmc.h"
/****************************************************************
* Signature of function under test
****************************************************************/
uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
size_t uxBufferLength,
BaseType_t xExpected );
/****************************************************************
* Abstraction of prvReadNameField proved in ReadNameField
****************************************************************/
size_t prvReadNameField( const uint8_t *pucByte,
size_t uxRemainingBytes,
char *pcName,
size_t uxDestLen )
{
__CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
__CPROVER_assert(NAME_SIZE < CBMC_MAX_OBJECT_SIZE,
"NAME_SIZE < CBMC_MAX_OBJECT_SIZE");
__CPROVER_assert(NAME_SIZE >= 4,
"NAME_SIZE >= 4 required for good coverage.");
/* Preconditions */
__CPROVER_assert(uxRemainingBytes < CBMC_MAX_OBJECT_SIZE,
"ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)");
__CPROVER_assert(uxDestLen < CBMC_MAX_OBJECT_SIZE,
"ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)");
__CPROVER_assert(uxRemainingBytes <= NETWORK_BUFFER_SIZE,
"ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)");
/* This precondition in the function contract for prvReadNameField
* fails because prvCheckOptions called prvReadNameField with the
* constant value 254.
__CPROVER_assert(uxDestLen <= NAME_SIZE,
"ReadNameField: uxDestLen <= NAME_SIZE)");
*/
__CPROVER_assert( pucByte != NULL ,
"ReadNameField: pucByte != NULL )");
__CPROVER_assert( pcName != NULL ,
"ReadNameField: pcName != NULL )");
__CPROVER_assert(uxDestLen > 0,
"ReadNameField: uxDestLen > 0)");
/* Return value */
size_t index;
/* Postconditions */
__CPROVER_assume( index <= uxDestLen+1 && index <= uxRemainingBytes );
return index;
}
/****************************************************************
* Abstraction of prvSkipNameField proved in SkipNameField
****************************************************************/
size_t prvSkipNameField( const uint8_t *pucByte, size_t uxLength )
{
__CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
/* Preconditions */
__CPROVER_assert(uxLength < CBMC_MAX_OBJECT_SIZE,
"SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)");
__CPROVER_assert(uxLength <= NETWORK_BUFFER_SIZE,
"SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)");
__CPROVER_assert(pucByte != NULL,
"SkipNameField: pucByte != NULL)");
/* Return value */
size_t index;
/* Postconditions */
__CPROVER_assume(index <= uxLength);
return index;
}
/****************************************************************
* Proof of prvParseDNSReply
****************************************************************/
void harness() {
size_t uxBufferLength;
BaseType_t xExpected;
uint8_t *pucUDPPayloadBuffer = malloc(uxBufferLength);
__CPROVER_assert(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE");
__CPROVER_assume(uxBufferLength < CBMC_MAX_OBJECT_SIZE);
__CPROVER_assume(uxBufferLength <= NETWORK_BUFFER_SIZE);
__CPROVER_assume(pucUDPPayloadBuffer != NULL);
uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer,
uxBufferLength,
xExpected );
}
|
