How to capture `foo_bar_offset` value for `bar` member of `foo` struct?

[Kiwamu Okabe]

Dear all,

I found `foo_bar_offset` value for `bar` member of `foo` struct. (See attached screenshot.)

How to capture it?

Now I'm trying to verify FreeRTOS code using VeriFast.

https://github.com/metasepi/amazon-freertos/

It can be verify with following command:

```

$ vfide -I verifast_inc lib/FreeRTOS/tasks.c

```

And I have written following predicate:

https://github.com/metasepi/amazon-freertos/blob/129971293c973d8d942156f285a9594c2f95c500/lib/FreeRTOS/tasks.c#L349

```

predicate TCB_t_pred(struct tskTaskControlBlock *tcb) =
    tcb->pxTopOfStack |-> _
    &*& tcb->uxPriority |-> _
    &*& tcb->pxStack |-> ?stack
    &*& StackType_pred(stack, _)
    &*& tcb->pxEndOfStack |-> _
    &*& tcb->uxCriticalNesting |-> _
    &*& tcb->ulRunTimeCounter |-> _
    &*& tcb->ucStaticallyAllocated |-> _
    &*& tcb->ucDelayAborted |-> _
    &*& malloc_block_tskTaskControlBlock(tcb);

```

I think above predicate should own heap chunks showed on the screenshot.

But following code causes an error:

```

$ vi lib/FreeRTOS/tasks.c

--snip--

/*@
predicate TCB_t_pred(struct tskTaskControlBlock *tcb) =
    tcb->pxTopOfStack |-> _
    &*& struct_xMPU_SETTINGS_padding((tcb + tskTaskControlBlock_xMPUSettings_offset))
--snip--

$ verifast -c -I verifast_inc lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c(352,45-84): No such variable, constructor, regular function, predicate, enum element, global variable, or module: tskTaskControlBlock_xMPUSettings_offset

```

How to fix it?

Best regards,

Kiwamu Okabe

[Bart Jacobs]

Instead of `(tcb + tskTaskControlBlock_xMPUSettings_offset)`, write `&tcb->xMPUSettings`.

[Kiwamu Okabe]

On Thu, Sep 6, 2018 at 5:10 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> Instead of `(tcb + tskTaskControlBlock_xMPUSettings_offset)`, write `&tcb->xMPUSettings`.

Thanks. it works.

```

/*@
predicate TCB_t_pred(struct tskTaskControlBlock *tcb) =
tcb->pxTopOfStack |-> _

&*& struct_xMPU_SETTINGS_padding(&tcb->xMPUSettings)
&*& struct_xLIST_ITEM_padding(&tcb->xStateListItem)
&*& struct_xLIST_ITEM_padding(&tcb->xEventListItem)

&*& tcb->uxPriority |-> _
&*& tcb->pxStack |-> ?stack
&*& StackType_pred(stack, _)

&*& chars(tcb->pcTaskName, 16, _)

&*& tcb->pxEndOfStack |-> _
&*& tcb->uxCriticalNesting |-> _

&*& pointers(tcb->pvThreadLocalStoragePointers, 1, _)

&*& tcb->ulRunTimeCounter |-> _
&*& tcb->ucStaticallyAllocated |-> _
&*& tcb->ucDelayAborted |-> _
&*& malloc_block_tskTaskControlBlock(tcb);

@*/
```

I'm little bit confusing. Because...

A. I used `&tcb->foo` at `struct_xLIST_ITEM_padding` chunk.
B. I used `tcb->foo` at `pointers` and `chars` chunk.

What are different? A and B are also showing following style on
the Heap chunks pane of attached screenshot:

```
pxNewTCB0 + foo_bar_offset
```

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Kiwamu Okabe]

On Thu, Sep 6, 2018 at 5:10 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:

> Instead of `(tcb + tskTaskControlBlock_xMPUSettings_offset)`, write `&tcb->xMPUSettings`.

Thanks. it works.

```

/*@
predicate TCB_t_pred(struct tskTaskControlBlock *tcb) =
tcb->pxTopOfStack |-> _

&*& struct_xMPU_SETTINGS_padding(&tcb->xMPUSettings)
&*& struct_xLIST_ITEM_padding(&tcb->xStateListItem)
&*& struct_xLIST_ITEM_padding(&tcb->xEventListItem)

&*& tcb->uxPriority |-> _
&*& tcb->pxStack |-> ?stack
&*& StackType_pred(stack, _)

&*& chars(tcb->pcTaskName, 16, _)

&*& tcb->pxEndOfStack |-> _
&*& tcb->uxCriticalNesting |-> _

&*& pointers(tcb->pvThreadLocalStoragePointers, 1, _)

&*& tcb->ulRunTimeCounter |-> _
&*& tcb->ucStaticallyAllocated |-> _
&*& tcb->ucDelayAborted |-> _
&*& malloc_block_tskTaskControlBlock(tcb);

[Bart Jacobs]

This corresponds to the way C treats arrays versus other variables: if variable `x` is of array type, then `x` used as an expression denotes the address of the array, whereas if `x` is not of array type it denotes the value of the variable.

On Thursday, September 6, 2018 at 9:57:51 AM UTC+2, Kiwamu Okabe wrote:

[Kiwamu Okabe]

On Thu, Sep 6, 2018 at 5:46 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> This corresponds to the way C treats arrays versus other variables: if variable `x` is of array type, then `x` used as an expression denotes the address of the array, whereas if `x` is not of array type it denotes the value of the variable.

I think I understand.
Thanks.