]> git.sur5r.net Git - freertos/blobdiff - FreeRTOS/Source/include/FreeRTOS.h
Fix spelling issues.
[freertos] / FreeRTOS / Source / include / FreeRTOS.h
index 45c778a0396e29389b76109e0960c9ab916d08f6..4df39db39cbf4db6a969c7fa9b1e409cab332d47 100644 (file)
@@ -241,10 +241,26 @@ extern "C" {
        #define configASSERT_DEFINED 1\r
 #endif\r
 \r
+/* configPRECONDITION should be defined as configASSERT.\r
+The CBMC proofs need a way to track assumptions and assertions.\r
+A configPRECONDITION statement should express an implicit invariant or\r
+assumption made.  A configASSERT statement should express an invariant that must\r
+hold explicit before calling the code. */\r
+#ifndef configPRECONDITION\r
+       #define configPRECONDITION( X ) configASSERT(X)\r
+       #define configPRECONDITION_DEFINED 0\r
+#else\r
+       #define configPRECONDITION_DEFINED 1\r
+#endif\r
+\r
 #ifndef portMEMORY_BARRIER\r
        #define portMEMORY_BARRIER()\r
 #endif\r
 \r
+#ifndef portSOFTWARE_BARRIER\r
+       #define portSOFTWARE_BARRIER()\r
+#endif\r
+\r
 /* The timers module relies on xTaskGetSchedulerState(). */\r
 #if configUSE_TIMERS == 1\r
 \r
@@ -937,6 +953,7 @@ V8 if desired. */
        #define pcTimerGetTimerName pcTimerGetName\r
        #define pcQueueGetQueueName pcQueueGetName\r
        #define vTaskGetTaskInfo vTaskGetInfo\r
+       #define xTaskGetIdleRunTimeCounter ulTaskGetIdleRunTimeCounter\r
 \r
        /* Backward compatibility within the scheduler code only - these definitions\r
        are not really required but are included for completeness. */\r