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
|
/*
* FreeRTOS memory safety proofs with CBMC.
* Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation
* files (the "Software"), to deal in the Software without
* restriction, including without limitation the rights to use, copy,
* modify, merge, publish, distribute, sublicense, and/or sell copies
* of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
* BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
* ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*
* http://aws.amazon.com/freertos
* http://www.FreeRTOS.org
*/
#include "FreeRTOS.h"
#include "queue.h"
#include "queue_init.h"
#include "cbmc.h"
#ifndef ITEM_BOUND
#define ITEM_BOUND 10
#endif
#if( configUSE_QUEUE_SETS == 0 )
BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
{
if(pxQueue->uxItemSize > ( UBaseType_t ) 0)
{
__CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable");
if(xPosition == queueSEND_TO_BACK){
__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable");
}else{
__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable");
}
return pdFALSE;
}else
{
return nondet_BaseType_t();
}
}
#endif
void harness(){
QueueHandle_t xQueue = xUnconstrainedQueueBoundedItemSize(ITEM_BOUND);
if( xQueue ){
void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize);
BaseType_t *xHigherPriorityTaskWoken = pvPortMalloc(sizeof(BaseType_t));
BaseType_t xCopyPosition;
if(xQueue->uxItemSize == 0)
{
/* uxQueue->xQueueType is a pointer to the head of the queue storage area.
If an item has a size, this pointer must not be modified after init.
Otherwise some of the write statements will fail. */
xQueue->uxQueueType = nondet_int8_t();
pvItemToQueue = 0;
}
/* This code checks explicitly for violations of the pxQueue->uxMessagesWaiting < pxQueue->uxLength
invariant. */
xQueue->uxMessagesWaiting = nondet_UBaseType_t();
if(!pvItemToQueue){
xQueue->uxItemSize = 0;
}
if(xCopyPosition == 2 ){
__CPROVER_assume(xQueue->uxLength == 1);
}
xQueueGenericSendFromISR( xQueue, pvItemToQueue, xHigherPriorityTaskWoken, xCopyPosition );
}
}
|
