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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 143, Issue 12



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>