len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Extended precondition of vListInsertEnd to prove absence of overflows.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-01 14:57:13 -05:00
parent 8976bd4d03
commit 9b2bb08cb5
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
list.c
View file

@ -95,7 +95,8 @@ void vListInsertEnd( List_t * const pxList,
// TODO: Adapt contract and proof to new version of predicates. // TODO: Adapt contract and proof to new version of predicates.
/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*& /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*&
xLIST_ITEM(pxNewListItem, ?val, _, _, ?ow, _);@*/ xLIST_ITEM(pxNewListItem, ?val, _, _, ?ow, _) &*&
len < INT_MAX;@*/
/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals, ?new_owners) &*& /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals, ?new_owners) &*&
idx == end idx == end
? (new_cells == append(cells, singleton(pxNewListItem)) &*& ? (new_cells == append(cells, singleton(pxNewListItem)) &*&