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

Used single-core list predicate xLIST to express access permissions to ready lists in readyLists_p.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-18 16:27:38 -05:00
parent 8f463be9d8
commit cf65065a0c
3 changed files with 43 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tasks.c
View file

@ -985,6 +985,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ open taskISRLockInv(); //@ open taskISRLockInv();
//@ open readyLists_p(); //@ open readyLists_p();
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
//@ List_array_get_l(pxReadyTasksLists, uxCurrentPriority);
//@ open xLIST(&pxReadyTasksLists[uxCurrentPriority], _, _, _, _, _);
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{ {

41
verification/verifast/proof/ready_list_predicates.h
View file

@ -1,17 +1,48 @@
#ifndef READY_LIST_PREDICATES_H #ifndef READY_LIST_PREDICATES_H
#define READY_LIST_PREDICATES_H #define READY_LIST_PREDICATES_H
#include "single_core_proofs/scp_list_predicates.h"
/*@ /*@
// TODO: Replace List_p by Aaloks list predicate
predicate List_array_p(List_t* array, int size) = predicate List_array_p(List_t* array, int size) =
size >= 0 &*&
size > 0
? (
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
size > 0 &*& xLIST(array,
List_p(array) &*& ?uxNumberOfItems,
size > 1 ?pxIndex,
? List_array_p(array + 1, size - 1) ?xListEnd,
?cells,
?vals)
&*&
List_array_p(array + 1, size - 1)
)
: true; : true;
lemma void List_array_get_l(List_t* array, int index)
requires List_array_p(array, ?size) &*&
0 <= index &*& index < size;
ensures List_array_p(array, index) &*&
pointer_within_limits(array) == true &*&
xLIST(array + index,
?uxNumberOfItems,
?pxIndex,
?xListEnd,
?cells,
?vals) &*&
List_array_p(array + index + 1, size-index-1);
{
if( index == 0) {
open List_array_p(array, size);
close List_array_p(array, 0);
} else {
open List_array_p(array, size);
List_array_get_l(array + 1, index - 1);
close List_array_p(array, index);
}
}
// For testing purposes only! // For testing purposes only!
// TODO: Replace by Aaloks list predicate // TODO: Replace by Aaloks list predicate
predicate List_p(List_t* l); predicate List_p(List_t* l);

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

@ -212,6 +212,8 @@ ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
} }
} }
#endif /* VERIFAST_TODO */
/*@
predicate xLIST( predicate xLIST(
struct xLIST *l, struct xLIST *l,
int uxNumberOfItems, int uxNumberOfItems,
@ -229,7 +231,9 @@ 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;