On Fri, Sep 7, 2018 at 6:42 PM Bart Jacobs <
bart....@cs.kuleuven.be> wrote:
> > I need to define some predicate for `struct xLIST`?
>
> Yes. Furthermore, you need to define a predicate for arrays of struct
> xLIST. For example:
> ```
> predicate xLISTs(struct xLIST *p, int count;) = count == 0 ? emp :
> xLIST(p) &*& xLISTs(p + 1, count - 1);
> ```
> where `xLIST` is the predicate you defined for `struct xLIST`.
Umm... I think it doesn't make sense.
Following patch occurs error:
```
$ pwd
/home/kiwamu/src/amazon-freertos-metasepi
$ git diff | cat
diff --git a/lib/FreeRTOS/tasks.c b/lib/FreeRTOS/tasks.c
index 6962b04..e6d6d3b 100644
--- a/lib/FreeRTOS/tasks.c
+++ b/lib/FreeRTOS/tasks.c
@@ -1068,8 +1068,8 @@ UBaseType_t x;
 /*-----------------------------------------------------------*/
 static void prvAddNewTaskToReadyList( TCB_t *pxNewTCB )
-    //@ requires u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*& TCB_t_pred(pxNewTCB);
-    //@ ensures u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _);
+    //@ requires u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*&
pxReadyTasksLists[..configMAX_PRIORITIES] |-> _ &*&
TCB_t_pred(pxNewTCB);
+    //@ ensures u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*&
pxReadyTasksLists[..configMAX_PRIORITIES] |-> _;
 {
        /* Ensure interrupts don't access the task lists while the
lists are being
        updated. */
diff --git a/verifast_inc/list.h b/verifast_inc/list.h
index d949694..c089947 100644
--- a/verifast_inc/list.h
+++ b/verifast_inc/list.h
@@ -14,8 +14,20 @@ typedef struct xLIST_ITEM ListItem_t;
 typedef struct xLIST
 {
+       int dummy;
 } List_t;
+/*@
+predicate xLIST(struct xLIST *p) =
+    p->dummy |-> _;
+
+predicate xLISTs(struct xLIST *p, int count;) =
+    count == 0 ?
+        emp
+    :
+        xLIST(p) &*& xLISTs(p + 1, count - 1);
+@*/
+
 #define listSET_LIST_ITEM_OWNER( pxListItem, pxOwner )         ( (
pxListItem )->pvOwner = ( void * ) ( pxOwner ) )
 #define listSET_LIST_ITEM_VALUE( pxListItem, xValue )  ( ( pxListItem
)->xItemValue = ( xValue ) )
$ verifast -c -I verifast_inc lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c
verifast_inc/list.h(28,9-14): Preciseness check failure: callee is not precise.
```
What does `precise` mean?