--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on May 2020 ---
If you want to prove things about C programs that do dynamic allocation you might want to try the Verified Software Toolchain, https://vst.cs.princeton.edu/. It uses separation logic and is based on the Coq proof assistant. However, it requires manual proving. Rich On Sun, May 17, 2020 at 1:10 AM < frama-c-discuss-request at lists.gforge.inria.fr> wrote: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > Today's Topics: > > 1. Use of ACSL types for WP (Whalen, Mike) > 2. Frama-c support for dynamic memory (Whalen, Mike) > > > > ---------- Forwarded message ---------- > From: "Whalen, Mike" <mww at amazon.com> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Cc: > Bcc: > Date: Sun, 17 May 2020 04:38:43 +0000 > Subject: [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 > > > > ---------- Forwarded message ---------- > From: "Whalen, Mike" <mww at amazon.com> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Cc: > Bcc: > Date: Sun, 17 May 2020 05:10:18 +0000 > Subject: [Frama-c-discuss] Frama-c support for dynamic memory > > I have made it to nearly the end of the WP tutorial. In chapter 8, it is > mentioned that âWP cannot currently work with dynamic allocation. A > function that would use it could not be proved.â > > I would move this to an earlier portion of the document, say, chapter 1. > This is quite disappointing. > > > > Are there any frama-c tools that do work with dynamic allocation? > > > > Mike > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200518/4725b832/attachment.html>