|
|
@ -94,6 +94,13 @@
|
|
|
|
#define configUSE_MALLOC_FAILED_HOOK 0
|
|
|
|
#define configUSE_MALLOC_FAILED_HOOK 0
|
|
|
|
#endif
|
|
|
|
#endif
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#ifndef configASSERT
|
|
|
|
|
|
|
|
#define configASSERT( x )
|
|
|
|
|
|
|
|
#define configASSERT_DEFINED 0
|
|
|
|
|
|
|
|
#else
|
|
|
|
|
|
|
|
#define configASSERT_DEFINED 1
|
|
|
|
|
|
|
|
#endif
|
|
|
|
|
|
|
|
|
|
|
|
/* Basic FreeRTOS definitions. */
|
|
|
|
/* Basic FreeRTOS definitions. */
|
|
|
|
#include "projdefs.h"
|
|
|
|
#include "projdefs.h"
|
|
|
|
|
|
|
|
|
|
|
@ -364,13 +371,6 @@
|
|
|
|
#error configMAX_TASK_NAME_LEN must be set to a minimum of 1 in FreeRTOSConfig.h
|
|
|
|
#error configMAX_TASK_NAME_LEN must be set to a minimum of 1 in FreeRTOSConfig.h
|
|
|
|
#endif
|
|
|
|
#endif
|
|
|
|
|
|
|
|
|
|
|
|
#ifndef configASSERT
|
|
|
|
|
|
|
|
#define configASSERT( x )
|
|
|
|
|
|
|
|
#define configASSERT_DEFINED 0
|
|
|
|
|
|
|
|
#else
|
|
|
|
|
|
|
|
#define configASSERT_DEFINED 1
|
|
|
|
|
|
|
|
#endif
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/* configPRECONDITION should be defined as configASSERT.
|
|
|
|
/* configPRECONDITION should be defined as configASSERT.
|
|
|
|
* The CBMC proofs need a way to track assumptions and assertions.
|
|
|
|
* The CBMC proofs need a way to track assumptions and assertions.
|
|
|
|
* A configPRECONDITION statement should express an implicit invariant or
|
|
|
|
* A configPRECONDITION statement should express an implicit invariant or
|
|
|
|