From a81bec40a58ce45101adcea98239964da5826ec1 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 31 Jan 2019 15:15:43 -0800 Subject: [PATCH 3/4] Replace MiniListItem_t with ListItem_t MiniListItem_t is intended to be the last element of a linked list. It saves space by having a payload but no `next' pointer, since there is no next element. CBMC gets confused when it sees a list of ListItem_ts with a smaller MiniListItem_t at the end, so this commit makes the last element of lists a ListItem_t instead. This patch should be removed soon: It is for a CBMC issue being fixed now. --- lib/include/private/list.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/include/private/list.h b/lib/include/private/list.h index 43e0ffffb..f6c6b6636 100644 --- a/lib/include/private/list.h +++ b/lib/include/private/list.h @@ -166,7 +166,7 @@ typedef struct xLIST listFIRST_LIST_INTEGRITY_CHECK_VALUE /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */ volatile UBaseType_t uxNumberOfItems; ListItem_t * configLIST_VOLATILE pxIndex; /*< Used to walk through the list. Points to the last item returned by a call to listGET_OWNER_OF_NEXT_ENTRY (). */ - MiniListItem_t xListEnd; /*< List item that contains the maximum possible item value meaning it is always at the end of the list and is therefore used as a marker. */ + ListItem_t xListEnd; listSECOND_LIST_INTEGRITY_CHECK_VALUE /*< Set to a known value if configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */ } List_t; -- 2.21.0