mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-12-11 22:25:14 -05:00
Added adaptation of Aalok's and Nathan's single-core proof for uxListRemove
This commit is contained in:
Tobias Reinhard
parent
6f782b494a
commit
cd3fa4e577
4 changed files with 484 additions and 7 deletions
477
list.c
477
list.c
|
|
@ -186,10 +186,154 @@ void vListInsert( List_t * const pxList,
|
||||||
/*-----------------------------------------------------------*/
|
/*-----------------------------------------------------------*/
|
||||||
|
|
||||||
UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
|
UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
|
||||||
{
|
#ifndef VERIFAST_SINGLE_CORE
|
||||||
|
/* Reason for rewrite:
|
||||||
|
* Predicates `xLIST_ITEM`, `DLS` and `xLIST` have been extended to expose
|
||||||
|
* node owners. Proofs using these predicates must be adapted as well.
|
||||||
|
*/
|
||||||
|
|
||||||
|
/*@requires
|
||||||
|
exists<struct xLIST * >(?l) &*&
|
||||||
|
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*&
|
||||||
|
end != pxItemToRemove &*&
|
||||||
|
mem(pxItemToRemove, cells) == true;@*/
|
||||||
|
/*@ensures
|
||||||
|
result == len-1 &*&
|
||||||
|
xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, nth(index_of(pxItemToRemove, cells), owners), NULL) &*&
|
||||||
|
pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*&
|
||||||
|
xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx, end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals), remove_nth(index_of(pxItemToRemove, cells), owners));
|
||||||
|
@*/
|
||||||
|
{
|
||||||
|
/* For brevity we alias x to pxItemToRemove */
|
||||||
|
/*@struct xLIST_ITEM *x = pxItemToRemove;@*/
|
||||||
|
|
||||||
|
/* Start by establishing that the list must be non-empty since x != end */
|
||||||
|
/*@open xLIST(l, len, idx, end, cells, vals, owners);@*/
|
||||||
|
/*@assert DLS(end, ?endprev, end, _, cells, vals, owners, l);@*/
|
||||||
|
/*@assert vals == cons(portMAX_DELAY, _);@*/
|
||||||
|
/*@dls_not_empty(end, endprev, cells, x);@*/
|
||||||
|
|
||||||
|
/* We know the xLIST is a DLS: end...endprev
|
||||||
|
Split this into DLS1:end...xprev and DLS2:x...endprev */
|
||||||
|
/*@int i = index_of(x, cells);@*/
|
||||||
|
/*@split(end, endprev, end, endprev, cells, vals, x, i);@*/
|
||||||
|
/*@list<struct xLIST_ITEM *> ys = take(i, cells);@*/
|
||||||
|
/*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
|
||||||
|
/*@list<TickType_t> vs = take(i, vals);@*/
|
||||||
|
/*@list<TickType_t> ws = drop(i, vals);@*/
|
||||||
|
/*@list<void*> ts = take(i, owners);@*/
|
||||||
|
/*@list<void*> us = drop(i, owners);@*/
|
||||||
|
/*@assert length(ys) == length(vs);@*/
|
||||||
|
/*@assert length(zs) == length(ws);@*/
|
||||||
|
/*@assert length(ts) == length(vs);@*/
|
||||||
|
/*@assert length(us) == length(ws);@*/
|
||||||
|
/*@assert DLS(end, endprev, x, ?xprev, ys, vs, ts, l);@*/ /*< DLS1 (ys, vs) */
|
||||||
|
/*@assert DLS(x, xprev, end, endprev, zs, ws, us, l);@*/ /*< DLS2 (zs, ws) */
|
||||||
|
|
||||||
|
/* Now case split to open DLS1 and DLS2 appropriately */
|
||||||
|
/*@
|
||||||
|
if (end == xprev)
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case A
|
||||||
|
//DLS1: extract end=prev=next
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, ts, l);
|
||||||
|
assert owners == cons(_, _);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, head(owners), l);
|
||||||
|
//DLS2: extract x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, us, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(ys) == 1;
|
||||||
|
assert length(zs) == 1;
|
||||||
|
assert length(us) == 1;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case B
|
||||||
|
//DLS1: extract end=prev
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, ts, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, head(owners), l);
|
||||||
|
//DLS2: extract next and x
|
||||||
|
open DLS(x, end, end, endprev, zs, ws, us, l);
|
||||||
|
assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l);
|
||||||
|
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l);
|
||||||
|
open xLIST_ITEM(xnext, _, _, x, _, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(ys) == 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case C
|
||||||
|
//DLS1: extract end=next and prev
|
||||||
|
dls_last_mem(end, endprev, x, xprev, ys);
|
||||||
|
assert mem(xprev, ys) == true;
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, ts, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, head(ts), l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, _, l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l);
|
||||||
|
int k = index_of(xprev, tail(ys));
|
||||||
|
dls_last_mem(endnext, end, x, xprev, tail(ys));
|
||||||
|
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
|
||||||
|
open DLS(xprev, _, x, xprev, _, _, _, l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, _, l);
|
||||||
|
}
|
||||||
|
//DLS2: extract x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, us, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(zs) == 1;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case D
|
||||||
|
//DLS1: extract prev
|
||||||
|
dls_last_mem(end, endprev, x, xprev, ys);
|
||||||
|
int j = index_of(xprev, ys);
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, ts, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, head(ts), l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l);
|
||||||
|
assert tail(ys) == singleton(xprev);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, _, l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), tail(ts), l);
|
||||||
|
int k = index_of(xprev, tail(ys));
|
||||||
|
dls_last_mem(endnext, end, x, xprev, tail(ys));
|
||||||
|
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
|
||||||
|
open DLS(xprev, _, x, xprev, _, _, _, l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, _, l);
|
||||||
|
}
|
||||||
|
//DLS2: extract next and x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, us, l);
|
||||||
|
assert xLIST_ITEM(x, _, ?xnext, _, _, l);
|
||||||
|
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), tail(us), l);
|
||||||
|
open xLIST_ITEM(xnext, _, _, x, _, l);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@drop_nth_index_of(vals, i);@*/
|
||||||
|
/*@drop_nth_index_of(owners, i);@*/
|
||||||
|
/*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, nth(i, owners), l);@*/
|
||||||
|
|
||||||
/* The list item knows which list it is in. Obtain the list from the list
|
/* The list item knows which list it is in. Obtain the list from the list
|
||||||
* item. */
|
* item. */
|
||||||
|
#ifdef VERIFAST /*< const pointer declaration */
|
||||||
|
List_t * pxList = pxItemToRemove->pxContainer;
|
||||||
|
#else
|
||||||
List_t * const pxList = pxItemToRemove->pxContainer;
|
List_t * const pxList = pxItemToRemove->pxContainer;
|
||||||
|
#endif
|
||||||
|
|
||||||
pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
|
pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
|
||||||
pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
|
pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
|
||||||
|
|
@ -211,5 +355,336 @@ UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
|
||||||
( pxList->uxNumberOfItems )--;
|
( pxList->uxNumberOfItems )--;
|
||||||
|
|
||||||
return pxList->uxNumberOfItems;
|
return pxList->uxNumberOfItems;
|
||||||
|
|
||||||
|
/*@
|
||||||
|
// Reassemble DLS1 and a modified DLS2, which no longer includes x
|
||||||
|
if (end == xprev)
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case A
|
||||||
|
close xLIST_ITEM(end, portMAX_DELAY, _, _, _, _);
|
||||||
|
close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), singleton(head(owners)), l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case B
|
||||||
|
close xLIST_ITEM(xprev, _, xnext, endprev, head(owners), l);
|
||||||
|
close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), singleton(head(owners)), l);
|
||||||
|
close xLIST_ITEM(xnext, _, _, xprev, _, l);
|
||||||
|
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), tail(us), l);
|
||||||
|
join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY),
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case C
|
||||||
|
close xLIST_ITEM(end, _, ?endnext, xprev, head(ts), l);
|
||||||
|
close xLIST_ITEM(xprev, ?xprev_val, end, _, ?xprev_owner, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l);
|
||||||
|
close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), cons(head(ts), singleton(xprev_owner)), l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l);
|
||||||
|
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, _, l);
|
||||||
|
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
|
||||||
|
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
|
||||||
|
close DLS(end, xprev, end, xprev, ys, vs, ts, l);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case D
|
||||||
|
close xLIST_ITEM(xnext, _, ?xnextnext, xprev, ?xnext_owner, l);
|
||||||
|
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), tail(us), l);
|
||||||
|
close xLIST_ITEM(end, _, ?endnext, endprev, head(ts), l);
|
||||||
|
close xLIST_ITEM(xprev, ?xprev_val, xnext, _, ?xprev_owner, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l);
|
||||||
|
close DLS(end, endprev, xnext, xprev, ys, vs, ts, l);
|
||||||
|
join(end, endprev, xnext, xprev, ys, vs,
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), singleton(xprev_owner), l);
|
||||||
|
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, _, l);
|
||||||
|
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
|
||||||
|
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
|
||||||
|
close DLS(end, endprev, xnext, xprev, ys, vs, ts, l);
|
||||||
|
join(end, endprev, xnext, xprev, ys, vs,
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@remove_remove_nth(cells, x);@*/
|
||||||
|
/*@
|
||||||
|
if (idx == x)
|
||||||
|
{
|
||||||
|
close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)), append(ts, tail(us)));
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
idx_remains_in_list(cells, idx, x, i);
|
||||||
|
close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)), append(ts, tail(us)));
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, nth(i, owners), NULL);@*/
|
||||||
}
|
}
|
||||||
|
#else
|
||||||
|
// Contract and proof written by Aalok Thakkar and Nathan Chong for the
|
||||||
|
// single-core setup in 2020.
|
||||||
|
|
||||||
|
/*@requires
|
||||||
|
exists<struct xLIST * >(?l) &*&
|
||||||
|
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
|
||||||
|
end != pxItemToRemove &*&
|
||||||
|
mem(pxItemToRemove, cells) == true;@*/
|
||||||
|
/*@ensures
|
||||||
|
result == len-1 &*&
|
||||||
|
xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, NULL) &*&
|
||||||
|
pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*&
|
||||||
|
xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx, end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals));@*/
|
||||||
|
{
|
||||||
|
/* For brevity we alias x to pxItemToRemove */
|
||||||
|
/*@struct xLIST_ITEM *x = pxItemToRemove;@*/
|
||||||
|
|
||||||
|
/* Start by establishing that the list must be non-empty since x != end */
|
||||||
|
/*@open xLIST(l, len, idx, end, cells, vals);@*/
|
||||||
|
/*@assert DLS(end, ?endprev, end, _, cells, vals, l);@*/
|
||||||
|
/*@assert vals == cons(portMAX_DELAY, _);@*/
|
||||||
|
/*@dls_not_empty(end, endprev, cells, x);@*/
|
||||||
|
|
||||||
|
/* We know the xLIST is a DLS: end...endprev
|
||||||
|
Split this into DLS1:end...xprev and DLS2:x...endprev */
|
||||||
|
/*@int i = index_of(x, cells);@*/
|
||||||
|
/*@split(end, endprev, end, endprev, cells, vals, x, i);@*/
|
||||||
|
/*@list<struct xLIST_ITEM *> ys = take(i, cells);@*/
|
||||||
|
/*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
|
||||||
|
/*@list<TickType_t> vs = take(i, vals);@*/
|
||||||
|
/*@list<TickType_t> ws = drop(i, vals);@*/
|
||||||
|
/*@assert length(ys) == length(vs);@*/
|
||||||
|
/*@assert length(zs) == length(ws);@*/
|
||||||
|
/*@assert DLS(end, endprev, x, ?xprev, ys, vs, l);@*/ /*< DLS1 (ys, vs) */
|
||||||
|
/*@assert DLS(x, xprev, end, endprev, zs, ws, l);@*/ /*< DLS2 (zs, ws) */
|
||||||
|
|
||||||
|
/* Now case split to open DLS1 and DLS2 appropriately */
|
||||||
|
/*@
|
||||||
|
if (end == xprev)
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case A
|
||||||
|
//DLS1: extract end=prev=next
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
|
||||||
|
//DLS2: extract x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(ys) == 1;
|
||||||
|
assert length(zs) == 1;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case B
|
||||||
|
//DLS1: extract end=prev
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
|
||||||
|
//DLS2: extract next and x
|
||||||
|
open DLS(x, end, end, endprev, zs, ws, l);
|
||||||
|
assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), l);
|
||||||
|
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
|
||||||
|
open xLIST_ITEM(xnext, _, _, x, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(ys) == 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case C
|
||||||
|
//DLS1: extract end=next and prev
|
||||||
|
dls_last_mem(end, endprev, x, xprev, ys);
|
||||||
|
assert mem(xprev, ys) == true;
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
|
||||||
|
int k = index_of(xprev, tail(ys));
|
||||||
|
dls_last_mem(endnext, end, x, xprev, tail(ys));
|
||||||
|
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
|
||||||
|
open DLS(xprev, _, x, xprev, _, _, l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, l);
|
||||||
|
}
|
||||||
|
//DLS2: extract x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, l);
|
||||||
|
//Lengths
|
||||||
|
assert length(zs) == 1;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case D
|
||||||
|
//DLS1: extract prev
|
||||||
|
dls_last_mem(end, endprev, x, xprev, ys);
|
||||||
|
int j = index_of(xprev, ys);
|
||||||
|
open DLS(end, endprev, x, xprev, ys, vs, l);
|
||||||
|
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
|
||||||
|
assert tail(ys) == singleton(xprev);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
|
||||||
|
int k = index_of(xprev, tail(ys));
|
||||||
|
dls_last_mem(endnext, end, x, xprev, tail(ys));
|
||||||
|
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
|
||||||
|
open DLS(xprev, _, x, xprev, _, _, l);
|
||||||
|
open xLIST_ITEM(xprev, _, x, _, l);
|
||||||
|
}
|
||||||
|
//DLS2: extract next and x
|
||||||
|
open DLS(x, xprev, end, endprev, zs, ws, l);
|
||||||
|
assert xLIST_ITEM(x, _, ?xnext, _, l);
|
||||||
|
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
|
||||||
|
open xLIST_ITEM(xnext, _, _, x, l);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@drop_nth_index_of(vals, i);@*/
|
||||||
|
/*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, l);@*/
|
||||||
|
|
||||||
|
/* The list item knows which list it is in. Obtain the list from the list
|
||||||
|
* item. */
|
||||||
|
#ifdef VERIFAST /*< const pointer declaration */
|
||||||
|
List_t * pxList = pxItemToRemove->pxContainer;
|
||||||
|
#else
|
||||||
|
List_t * const pxList = pxItemToRemove->pxContainer;
|
||||||
|
#endif
|
||||||
|
|
||||||
|
pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
|
||||||
|
pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
|
||||||
|
|
||||||
|
/* Only used during decision coverage testing. */
|
||||||
|
mtCOVERAGE_TEST_DELAY();
|
||||||
|
|
||||||
|
/* Make sure the index is left pointing to a valid item. */
|
||||||
|
if( pxList->pxIndex == pxItemToRemove )
|
||||||
|
{
|
||||||
|
pxList->pxIndex = pxItemToRemove->pxPrevious;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
mtCOVERAGE_TEST_MARKER();
|
||||||
|
}
|
||||||
|
|
||||||
|
pxItemToRemove->pxContainer = NULL;
|
||||||
|
( pxList->uxNumberOfItems )--;
|
||||||
|
|
||||||
|
return pxList->uxNumberOfItems;
|
||||||
|
|
||||||
|
/*@
|
||||||
|
// Reassemble DLS1 and a modified DLS2, which no longer includes x
|
||||||
|
if (end == xprev)
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case A
|
||||||
|
close xLIST_ITEM(end, portMAX_DELAY, _, _, _);
|
||||||
|
close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case B
|
||||||
|
close xLIST_ITEM(xprev, _, xnext, endprev, l);
|
||||||
|
close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), l);
|
||||||
|
close xLIST_ITEM(xnext, _, _, xprev, l);
|
||||||
|
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
|
||||||
|
join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY),
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (x == endprev)
|
||||||
|
{
|
||||||
|
//Case C
|
||||||
|
close xLIST_ITEM(end, _, ?endnext, xprev, l);
|
||||||
|
close xLIST_ITEM(xprev, ?xprev_val, end, _, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), l);
|
||||||
|
close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), l);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
|
||||||
|
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
|
||||||
|
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
|
||||||
|
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
|
||||||
|
close DLS(end, xprev, end, xprev, ys, vs, l);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
//Case D
|
||||||
|
close xLIST_ITEM(xnext, _, ?xnextnext, xprev, l);
|
||||||
|
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
|
||||||
|
close xLIST_ITEM(end, _, ?endnext, endprev, l);
|
||||||
|
close xLIST_ITEM(xprev, ?xprev_val, xnext, _, l);
|
||||||
|
if (endnext == xprev)
|
||||||
|
{
|
||||||
|
close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
|
||||||
|
close DLS(end, endprev, xnext, xprev, ys, vs, l);
|
||||||
|
join(end, endprev, xnext, xprev, ys, vs,
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
|
||||||
|
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
|
||||||
|
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
|
||||||
|
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
|
||||||
|
close DLS(end, endprev, xnext, xprev, ys, vs, l);
|
||||||
|
join(end, endprev, xnext, xprev, ys, vs,
|
||||||
|
xnext, xprev, end, endprev, tail(zs), tail(ws));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@remove_remove_nth(cells, x);@*/
|
||||||
|
/*@
|
||||||
|
if (idx == x)
|
||||||
|
{
|
||||||
|
close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)));
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
idx_remains_in_list(cells, idx, x, i);
|
||||||
|
close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)));
|
||||||
|
}
|
||||||
|
@*/
|
||||||
|
/*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, NULL);@*/
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
#endif /* VERIFAST_SINGLE_CORE */
|
||||||
|
|
||||||
/*-----------------------------------------------------------*/
|
/*-----------------------------------------------------------*/
|
||||||
|
|
|
||||||
7
tasks.c
7
tasks.c
|
|
@ -31,13 +31,14 @@
|
||||||
|
|
||||||
//@ #include <bitops.gh>
|
//@ #include <bitops.gh>
|
||||||
//@ #include "list.gh"
|
//@ #include "list.gh"
|
||||||
|
//@ #include <listex.gh>
|
||||||
|
|
||||||
/* The following includes will be visible to VeriFast in the preprocessed
|
/* The following includes will be visible to VeriFast in the preprocessed
|
||||||
* code. VeriFast requires includes to occur befor definitions. Hence,
|
* code. VeriFast requires includes to occur befor definitions. Hence,
|
||||||
* all includes visible to VeriFast must occur before the preprocessed
|
* all includes visible to VeriFast must occur before the preprocessed
|
||||||
* ones.
|
* ones.
|
||||||
*/
|
*/
|
||||||
//VF_include #include "FreeRTOSConfig.h"
|
//VF_macro #include "FreeRTOSConfig.h"
|
||||||
|
|
||||||
//VF_macro #define NULL 0
|
//VF_macro #define NULL 0
|
||||||
#endif /* VERIFAST */
|
#endif /* VERIFAST */
|
||||||
|
|
@ -1217,8 +1218,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
|
||||||
|
|
||||||
if( xTaskScheduled != pdFALSE )
|
if( xTaskScheduled != pdFALSE )
|
||||||
{
|
{
|
||||||
|
//@ close exists(gReadyList);
|
||||||
|
|
||||||
/* Once a task has been selected to run on this core,
|
/* Once a task has been selected to run on this core,
|
||||||
* move it to the end of the ready task list. */
|
* move it to the end of the ready task list. */
|
||||||
uxListRemove( pxTaskItem );
|
uxListRemove( pxTaskItem );
|
||||||
|
|
|
||||||
|
|
@ -60,9 +60,6 @@ fixpoint list<t> singleton<t>(t x) {
|
||||||
return cons(x, nil);
|
return cons(x, nil);
|
||||||
}
|
}
|
||||||
|
|
||||||
@*/
|
|
||||||
#ifdef VERIFAST_TODO
|
|
||||||
|
|
||||||
lemma void note(bool b)
|
lemma void note(bool b)
|
||||||
requires b;
|
requires b;
|
||||||
ensures b;
|
ensures b;
|
||||||
|
|
@ -630,6 +627,6 @@ lemma void combine_list_update<t>(list<t>prefix, t x, list<t>suffix, int i, list
|
||||||
}
|
}
|
||||||
|
|
||||||
@*/
|
@*/
|
||||||
#endif /* VERIFAST_TODO */
|
|
||||||
|
|
||||||
#endif /* SCP_COMMON_H */
|
#endif /* SCP_COMMON_H */
|
||||||
|
|
|
||||||
|
|
@ -683,7 +683,7 @@
|
||||||
@*/
|
@*/
|
||||||
#endif /* VERIFAST_SINGLE_CORE */
|
#endif /* VERIFAST_SINGLE_CORE */
|
||||||
|
|
||||||
#ifdef VERIFAST_TODO
|
/*@
|
||||||
lemma void idx_remains_in_list<t>(
|
lemma void idx_remains_in_list<t>(
|
||||||
list<t> cells,
|
list<t> cells,
|
||||||
t idx,
|
t idx,
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue