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

Finished proof of DLS_close_2.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-28 09:16:08 -05:00
parent 1393ae3c34
commit bb00bee690
1 changed files with 106 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

109
verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
View file

@ -680,13 +680,39 @@ ensures
// -> non-empty prefix // -> non-empty prefix
// (potentially empty suffix) // (potentially empty suffix)
open DLS_prefix(gPrefCells, gPrefVals, pxItem, gItemPrev,
gEnd, gEndPrev, gList);
if( gSufCells == nil ) {
// pxItem is the last/ right-most item in the list
// -> empty suffix
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd,
gEndPrev, gList);
assert( pxItem == gEndPrev );
close DLS(pxItem, gItemPrev, gEnd, gEndPrev,
singleton(pxItem), singleton(gItemVal), gList);
join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals,
pxItem, gItemPrev, gEnd, gEndPrev,
singleton(pxItem), singleton(gItemVal));
} else {
// pxItem is not the last/ right-most item in the list
// -> non-empty suffix
open DLS_suffix(gSufCells, gSufVals, pxItem, gItemNext, gEnd,
gEndPrev, gList);
close DLS(pxItem, gItemPrev, gEnd, gEndPrev,
cons(pxItem, gSufCells), cons(gItemVal, gSufVals),
gList);
join(gEnd, gEndPrev, pxItem, gItemPrev, gPrefCells, gPrefVals,
pxItem, gItemPrev, gEnd, gEndPrev,
cons(pxItem, gSufCells), cons(gItemVal, gSufVals));
}
} }
} }
@*/ @*/
void lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem) struct xLIST_ITEM* lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem)
/*@ requires /*@ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
@ -696,30 +722,103 @@ void lemma_validation__DLS_item_next_2(struct xLIST_ITEM* pxTaskItem)
@*/ @*/
/*@ ensures /*@ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*&
mem(pxTaskItem, gCells) == true; mem(pxTaskItem, gCells) == true &*&
mem(result, gCells) == true;
@*/ @*/
{ {
//@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem;
// first iteration step
//@ DLS_open_2(gTaskItem_0); //@ DLS_open_2(gTaskItem_0);
/*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val, /*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val,
?gTaskItem_0_next, ?gTaskItem_0_prev, gList) ); ?gTaskItem_0_next, ?gTaskItem_0_prev, gList) );
@*/ @*/
pxTaskItem = pxTaskItem->pxNext; pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* pxItem_1 = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val, /*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val,
gTaskItem_0_next, gTaskItem_0_prev, gList); gTaskItem_0_next, gTaskItem_0_prev, gList);
@*/ @*/
//@ DLS_close_2(gTaskItem_0, gCells, gVals); //@ DLS_close_2(gTaskItem_0, gCells, gVals);
//@ assert( mem(pxItem_1, gCells) == true ); // second iteration step
//@ DLS_open_2(gTaskItem_1);
/*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val,
?gTaskItem_1_next, ?gTaskItem_1_prev, gList) );
@*/
pxTaskItem = pxTaskItem->pxNext;
//@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val,
gTaskItem_1_next, gTaskItem_1_prev, gList);
@*/
//@ DLS_close_2(gTaskItem_1, gCells, gVals);
//@ assert( mem(gTaskItem_2, gCells) == true );
return pxTaskItem;
}
struct xLIST_ITEM* lemma_validation__DLS_item_prev_2(struct xLIST_ITEM* pxTaskItem)
/*@ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*&
mem(pxTaskItem, gCells) == true &*&
gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*&
length(gCells) > 1;
@*/
/*@ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*&
mem(pxTaskItem, gCells) == true &*&
mem(result, gCells) == true;
@*/
{
//@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem;
// first iteration step
//@ DLS_open_2(gTaskItem_0);
/*@ assert( xLIST_ITEM(gTaskItem_0, ?gTaskItem_0_val,
?gTaskItem_0_next, ?gTaskItem_0_prev, gList) );
@*/
pxTaskItem = pxTaskItem->pxPrevious;
//@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_0, gTaskItem_0_val,
gTaskItem_0_next, gTaskItem_0_prev, gList);
@*/
//@ DLS_close_2(gTaskItem_0, gCells, gVals);
// second iteration step
//@ DLS_open_2(gTaskItem_1);
/*@ assert( xLIST_ITEM(gTaskItem_1, ?gTaskItem_1_val,
?gTaskItem_1_next, ?gTaskItem_1_prev, gList) );
@*/
pxTaskItem = pxTaskItem->pxPrevious;
//@ struct xLIST_ITEM* gTaskItem_2 = pxTaskItem;
/*@ close xLIST_ITEM(gTaskItem_1, gTaskItem_1_val,
gTaskItem_1_next, gTaskItem_1_prev, gList);
@*/
//@ DLS_close_2(gTaskItem_1, gCells, gVals);
//@ assert( mem(gTaskItem_2, gCells) == true );
return pxTaskItem;
} }
#endif /* SCP_LIST_PREDICATES_EXTENDED_H */ #endif /* SCP_LIST_PREDICATES_EXTENDED_H */