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

Added more DLS lemmas.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-21 08:16:28 -05:00
parent 5cf8b4ed1c
commit 3fee2ec01f
1 changed files with 3 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

9
verification/verifast/proof/single_core_proofs/scp_list_predicates.h
View file

@ -230,9 +230,7 @@ predicate xLIST(
length(cells) == length(vals) &*& length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*& uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l); DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
@*/
#ifdef VERIFAST_TODO
lemma void xLIST_distinct_cells(struct xLIST *l) lemma void xLIST_distinct_cells(struct xLIST *l)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals); requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true; ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
@ -285,8 +283,6 @@ ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
close DLS(n, m, n, m, cells, vals, l); close DLS(n, m, n, m, cells, vals, l);
} }
#endif /* VERIFAST_TODO */
/*@
lemma void dls_last_mem( lemma void dls_last_mem(
struct xLIST_ITEM *n, struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev, struct xLIST_ITEM *nprev,
@ -342,8 +338,7 @@ ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xp
close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l); close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
} }
} }
@*/
#ifdef VERIFAST_TODO
lemma void join( lemma void join(
struct xLIST_ITEM *n1, struct xLIST_ITEM *n1,
struct xLIST_ITEM *nprev1, struct xLIST_ITEM *nprev1,
@ -380,7 +375,9 @@ ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2)
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l); close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
} }
} }
@*/
#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,