Skip to content

Commit b4aa81b

Browse files
dc42dc42
committed
Added minimal eCv annotations to allow client code to be verified
1 parent 89e9fe0 commit b4aa81b

File tree

9 files changed

+30
-17
lines changed

9 files changed

+30
-17
lines changed

‎src/include/FreeRTOS.h‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,19 @@
2828
#ifndef INC_FREERTOS_H
2929
#define INC_FREERTOS_H
3030

31+
#ifndef __ECV__
32+
// We use only a few eCv annotations so instead of including ecv.h we define them here
33+
# ifndef _ecv_from
34+
# define _ecv_from
35+
# endif
36+
# ifndef _ecv_array
37+
# define _ecv_array
38+
# endif
39+
# ifndef _ecv_null
40+
# define _ecv_null
41+
# endif
42+
#endif
43+
3144
/*
3245
* Include the generic headers required for the FreeRTOS port being used.
3346
*/

‎src/include/queue.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -647,7 +647,7 @@ typedef struct QueueDefinition * QueueSetMemberHandle_t;
647647
* \defgroup xQueueSend xQueueSend
648648
* \ingroup QueueManagement
649649
*/
650-
BaseType_t xQueueGenericSend( QueueHandle_t xQueue, const void * const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
650+
BaseType_t xQueueGenericSend( QueueHandle_t xQueue, const void *_ecv_null const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
651651

652652
/**
653653
* queue. h
@@ -1412,7 +1412,7 @@ BaseType_t xQueueCRReceive( QueueHandle_t xQueue, void *pvBuffer, TickType_t xTi
14121412
* these functions directly.
14131413
*/
14141414
QueueHandle_t xQueueCreateMutex( const uint8_t ucQueueType ) PRIVILEGED_FUNCTION;
1415-
QueueHandle_t xQueueCreateMutexStatic( const uint8_t ucQueueType, StaticQueue_t *pxStaticQueue ) PRIVILEGED_FUNCTION;
1415+
QueueHandle_t xQueueCreateMutexStatic( const uint8_t ucQueueType, StaticQueue_t *_ecv_from pxStaticQueue ) PRIVILEGED_FUNCTION;
14161416
QueueHandle_t xQueueCreateCountingSemaphore( const UBaseType_t uxMaxCount, const UBaseType_t uxInitialCount ) PRIVILEGED_FUNCTION;
14171417
QueueHandle_t xQueueCreateCountingSemaphoreStatic( const UBaseType_t uxMaxCount, const UBaseType_t uxInitialCount, StaticQueue_t *pxStaticQueue ) PRIVILEGED_FUNCTION;
14181418
BaseType_t xQueueSemaphoreTake( QueueHandle_t xQueue, TickType_t xTicksToWait ) PRIVILEGED_FUNCTION;
@@ -1502,7 +1502,7 @@ BaseType_t xQueueGiveMutexRecursive( QueueHandle_t xMutex ) PRIVILEGED_FUNCTION;
15021502
* RTOS objects that use the queue structure as their base.
15031503
*/
15041504
#if( configSUPPORT_STATIC_ALLOCATION == 1 )
1505-
QueueHandle_t xQueueGenericCreateStatic( const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, uint8_t *pucQueueStorage, StaticQueue_t *pxStaticQueue, const uint8_t ucQueueType ) PRIVILEGED_FUNCTION;
1505+
QueueHandle_t xQueueGenericCreateStatic( const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, uint8_t *_ecv_array _ecv_null pucQueueStorage, StaticQueue_t *_ecv_from pxStaticQueue, const uint8_t ucQueueType ) PRIVILEGED_FUNCTION;
15061506
#endif
15071507

15081508
/*

‎src/include/task.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ extern "C" {
6767
* \ingroup Tasks
6868
*/
6969
struct tskTaskControlBlock; /* The old naming convention is used to prevent breaking kernel aware debuggers. */
70-
typedef struct tskTaskControlBlock* TaskHandle_t;
70+
typedef struct tskTaskControlBlock *_ecv_from TaskHandle_t;
7171

7272
/*
7373
* Defines the prototype to which the application task hook function must
@@ -448,8 +448,8 @@ is used in assert() statements. */
448448
const uint32_t ulStackDepth,
449449
void * const pvParameters,
450450
UBaseType_t uxPriority,
451-
StackType_t * const puxStackBuffer,
452-
StaticTask_t * const pxTaskBuffer ) PRIVILEGED_FUNCTION;
451+
StackType_t *_ecv_array const puxStackBuffer,
452+
StaticTask_t *_ecv_from const pxTaskBuffer ) PRIVILEGED_FUNCTION;
453453
#endif /* configSUPPORT_STATIC_ALLOCATION */
454454

455455
/**
@@ -1850,7 +1850,7 @@ uint32_t ulTaskGetIdleRunTimeCounter( void ) PRIVILEGED_FUNCTION;
18501850
* \defgroup xTaskNotify xTaskNotify
18511851
* \ingroup TaskNotifications
18521852
*/
1853-
BaseType_t xTaskGenericNotify( TaskHandle_t xTaskToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t *pulPreviousNotificationValue ) PRIVILEGED_FUNCTION;
1853+
BaseType_t xTaskGenericNotify( TaskHandle_t xTaskToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t *_ecv_null pulPreviousNotificationValue ) PRIVILEGED_FUNCTION;
18541854
#define xTaskNotify( xTaskToNotify, ulValue, eAction ) xTaskGenericNotify( ( xTaskToNotify ), ( ulValue ), ( eAction ), NULL )
18551855
#define xTaskNotifyAndQuery( xTaskToNotify, ulValue, eAction, pulPreviousNotifyValue ) xTaskGenericNotify( ( xTaskToNotify ), ( ulValue ), ( eAction ), ( pulPreviousNotifyValue ) )
18561856

‎src/portable/GCC/ARM_CM0/port.c‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,11 @@
3434
#include "task.h"
3535

3636
/* Constants required to manipulate the NVIC. */
37-
#define portNVIC_SYSTICK_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000e010 ) )
38-
#define portNVIC_SYSTICK_LOAD_REG ( * ( ( volatile uint32_t * ) 0xe000e014 ) )
39-
#define portNVIC_SYSTICK_CURRENT_VALUE_REG ( * ( ( volatile uint32_t * ) 0xe000e018 ) )
40-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
41-
#define portNVIC_SYSPRI2_REG ( * ( ( volatile uint32_t * ) 0xe000ed20 ) )
37+
#define portNVIC_SYSTICK_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000e010u ) )
38+
#define portNVIC_SYSTICK_LOAD_REG ( * ( ( volatile uint32_t * ) 0xe000e014u ) )
39+
#define portNVIC_SYSTICK_CURRENT_VALUE_REG ( * ( ( volatile uint32_t * ) 0xe000e018u ) )
40+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
41+
#define portNVIC_SYSPRI2_REG ( * ( ( volatile uint32_t * ) 0xe000ed20u ) )
4242
#define portNVIC_SYSTICK_CLK_BIT ( 1UL << 2UL )
4343
#define portNVIC_SYSTICK_INT_BIT ( 1UL << 1UL )
4444
#define portNVIC_SYSTICK_ENABLE_BIT ( 1UL << 0UL )

‎src/portable/GCC/ARM_CM0/portmacro.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ typedef unsigned long UBaseType_t;
7878

7979
/* Scheduler utilities. */
8080
extern void vPortYield( void );
81-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
81+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
8282
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
8383
#define portYIELD() vPortYield()
8484
#define portEND_SWITCHING_ISR( xSwitchRequired ) if( xSwitchRequired ) portNVIC_INT_CTRL_REG = portNVIC_PENDSVSET_BIT

‎src/portable/GCC/ARM_CM3/portmacro.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ typedef unsigned long UBaseType_t;
8787
__asm volatile( "isb" ); \
8888
}
8989

90-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
90+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
9191
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
9292
#define portEND_SWITCHING_ISR( xSwitchRequired ) if( xSwitchRequired != pdFALSE ) portYIELD()
9393
#define portYIELD_FROM_ISR( x ) portEND_SWITCHING_ISR( x )

‎src/portable/GCC/ARM_CM4F/portmacro.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ typedef unsigned long UBaseType_t;
8787
__asm volatile( "isb" ); \
8888
}
8989

90-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
90+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
9191
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
9292
#define portEND_SWITCHING_ISR( xSwitchRequired ) if( xSwitchRequired != pdFALSE ) portYIELD()
9393
#define portYIELD_FROM_ISR( x ) portEND_SWITCHING_ISR( x )

‎src/portable/GCC/ARM_CM4_MPU/portmacro.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ typedef struct MPU_SETTINGS
130130
__asm volatile( "isb" ); \
131131
}
132132

133-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
133+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
134134
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
135135
#define portEND_SWITCHING_ISR( xSwitchRequired ) if( xSwitchRequired ) portNVIC_INT_CTRL_REG = portNVIC_PENDSVSET_BIT
136136
#define portYIELD_FROM_ISR( x ) portEND_SWITCHING_ISR( x )

‎src/portable/GCC/ARM_CM7/r0p1/portmacro.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ typedef unsigned long UBaseType_t;
8787
__asm volatile( "isb" ); \
8888
}
8989

90-
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04 ) )
90+
#define portNVIC_INT_CTRL_REG ( * ( ( volatile uint32_t * ) 0xe000ed04u ) )
9191
#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL )
9292
#define portEND_SWITCHING_ISR( xSwitchRequired ) if( xSwitchRequired != pdFALSE ) portYIELD()
9393
#define portYIELD_FROM_ISR( x ) portEND_SWITCHING_ISR( x )

0 commit comments

Comments
 (0)