--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on May 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Use of ACSL types for WP



I have a general question about representation types in frama-c.  I have a circular buffer of integers that is designed to represent a fifo queue.  I’d like to map it to a \list<int> and show that manipulations on the circular buffer preserve the abstract behavior of the list.  I notice that ACSL has a \list type that would seem to meet my needs.  However, I am not seeing how to create an abstract representation of the buffer.

My initial thought would be to put a ghost field of type \list<int> in the structure that defines a circular buffer.  However, it appears that ghost fields of any kind are not supported, unless I am misunderstanding the syntax in the ACSL manual:


// ghost field format matches the format

// in ACSL ANSI/ISO C Specification Language Version 1.14 document

// p. 99

typedef struct _foo {

    int field1;

    //@ ghost int bar;

    int field2;

} foo;

This does not compile using frama-c -wp test_ghost_field.c.

Next I thought I would just create ghost vars in the functions that modify the circular buffer and sync up that way, but it appears that \lists are not supported as ghost vars:

#include <stdio.h>

int main() {
    int x = 1;
    //@ ghost y = 2;
    //@ ghost y = y + 1;

    //@ ghost \list<int> z = [| |];
}

Frama-c will not compile this using: frama-c -wp test_ghost_list.c.

So…how *does* one create a type abstraction in frama-c/wp?  If there aren’t some good ways of abstracting types, I would expect reasoning to become complex, but perhaps I am approaching this the wrong way.  Any guidance or pointers is appreciated.

Thanks much,

Mike
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200517/ec9d5298/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_ghost_field.c
Type: application/octet-stream
Size: 333 bytes
Desc: test_ghost_field.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200517/ec9d5298/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_ghost_list.c
Type: application/octet-stream
Size: 214 bytes
Desc: test_ghost_list.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200517/ec9d5298/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: circ_buffer.c
Type: application/octet-stream
Size: 2168 bytes
Desc: circ_buffer.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200517/ec9d5298/attachment-0002.obj>