From eb5c60c60bec9af47987d4347cc741b81673b95b Mon Sep 17 00:00:00 2001 From: "Yuhui.Zheng" <10982575+yuhui-zheng@users.noreply.github.com> Date: Tue, 24 Sep 2019 22:29:35 +0000 Subject: [PATCH] Update FreeRTOS.h with the version in GitHub. This is also to test submodule. --- FreeRTOS/Source/include/FreeRTOS.h | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/FreeRTOS/Source/include/FreeRTOS.h b/FreeRTOS/Source/include/FreeRTOS.h index 14f98d0b0..ee60853f9 100644 --- a/FreeRTOS/Source/include/FreeRTOS.h +++ b/FreeRTOS/Source/include/FreeRTOS.h @@ -241,12 +241,11 @@ extern "C" { #define configASSERT_DEFINED 1 #endif -/* configPRECONDITION should resolve to configASSERT. The CBMC proofs need a way -to track assumptions and assertions. -- A configPRECONDITION statement should express an implicit invariant or -assumption made. -- A configASSERT statement should express an invariant that must hold explicit -before calling the code. */ +/* configPRECONDITION should be resolve to configASSERT. + The CBMC proofs need a way to track assumptions and assertions. + A configPRECONDITION statement should express an implicit invariant or assumption made. + A configASSERT statement should express an invariant that must hold explicit before calling + the code. */ #ifndef configPRECONDITION #define configPRECONDITION( X ) configASSERT(X) #define configPRECONDITION_DEFINED 0