--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on May 2020 ---
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>