#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
#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