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 "queue.h"
9 #include "semphr.h"
10
11 #include "cbmc.h"
12
13 /****************************************************************
14 * This is a collection of abstractions of methods in the FreeRTOS Kernel
15 * API. The abstractions simply perform minimal validation of
16 * function arguments, and return unconstrained values of the
17 * appropriate type.
18 ****************************************************************/
19
20 /****************************************************************
21 * Abstract vTaskSuspendAll
22 ****************************************************************/
vTaskSuspendAll(void)23 void vTaskSuspendAll( void )
24 {
25 }
26
27 /****************************************************************/
28
29 /****************************************************************
30 * Abstract vPortEnterCritical
31 ****************************************************************/
vPortEnterCritical(void)32 void vPortEnterCritical( void )
33 {
34 }
35
36 /****************************************************************/
37
38 /****************************************************************
39 * Abstract vListInsertEnd
40 ****************************************************************/
vListInsertEnd(List_t * const pxList,ListItem_t * const pxNewListItem)41 void vListInsertEnd( List_t * const pxList,
42 ListItem_t * const pxNewListItem )
43 {
44 }
45
46 /****************************************************************/
47
48 /****************************************************************
49 * Abstract vPortExitCritical
50 ****************************************************************/
vPortExitCritical(void)51 void vPortExitCritical( void )
52 {
53 }
54
55 /****************************************************************/
56
57 /****************************************************************
58 * Abstract xTaskResumeAll
59 ****************************************************************/
xTaskResumeAll(void)60 BaseType_t xTaskResumeAll( void )
61 {
62 BaseType_t xReturn;
63
64 __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
65
66 return xReturn;
67 }
68
69 /****************************************************************/
70
71 /****************************************************************
72 * Abstract xEventGroupSetBits
73 ****************************************************************/
xEventGroupSetBits(EventGroupHandle_t xEventGroup,const EventBits_t uxBitsToSet)74 EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup,
75 const EventBits_t uxBitsToSet )
76 {
77 EventBits_t xReturn;
78
79 return xReturn;
80 }
81
82 /****************************************************************/
83
