Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Having trouble proving a (seemingly) simple program

Thank you.  This is very helpful, not only for this particular case but for understanding the thought process to achieve a valid proof.

I still have much learning to do, but with your help I managed to get a simple list implementation validated (as far as internal consistency, not all storage semantics).  Loops are still a challenge for me, but with practice I think I can construct proofs and recognize where the underlying code needs adjustment to be provably correct.

Thanks again for your help.

-Jamie



From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> On Behalf Of Allan Blanchard
Sent: Wednesday, October 24, 2018 1:49 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] Having trouble proving a (seemingly) simple program


Hello,

The proof failure is due to a lack of separation, but let see how to find this out easily.

The assertion that fails contains memory accesses, so first, let us remove these accesses and replace them with local variables (doing this, they cannot be affected by the statement that modifies the memory).

//@ ghost void** g_content = list->content ;
//@ ghost int g_capacity = list->capacity ;
//@ assert \valid(list->content + (0..list->capacity-1));

list->content[list->count] = data;
//@ assert WITH_GHOST: \valid(g_content + (0 .. g_capacity-1));
//@ assert \valid(list->content + (0..list->capacity-1));

By doing this, we see that the assertion WITH_GHOST succeeds, and that the second one fails, meaning that one of the two memory accesses does not give the same value anymore, and we can add two assertions to know which one :

list->content[list->count] = data;
//@ assert FAILS: g_content == list->content ;
//@ assert g_capacity == list->capacity ;
//@ assert \valid(g_content + (0 .. g_capacity-1));
//@ assert \valid(list->content + (0..list->capacity-1));

And we see that the assertion named FAILS fails. That means that WP considers that the previous access can modify this memory regions, meaning that it does not know that &(list->content) and &(list->content[list->count]) (and more generally &(list->content[0 .. list->capacity-1])) are separated memory regions, which we can add in the precondition:

/*@
  //...
  requires \separated(list, list->content, list->content + (0 .. list->capacity));
  //...
*/

And then the program is proved :)  (and we can remove all the assertions).

Regards,
Allan
On 23/10/2018 22:29, Jamie Kawabata wrote:
Hello, I apologize if this is a newbie question, but I am experimenting with frama-c and WP and I am struggling with a simple problem.  Below is my program.

I am running under linux with the command line "frama-c-gui -wp -rte myproram.c"

The post-condition for AddTail is not being validated, in particular it is unable to prove \valid(list->content + (0..list->capacity-1)).
This condition is part of the precondition and remains provable until list->content[list->count] = data;
I thought perhaps it was a possible aliasing issue, if list->content could overlap with list, hence I tried requires \separated, but it is still failing to prove the postcondition.
I did find that if I store a list of floats instead of void*, the program validates, so I suppose it's using (or failing to use) the type inference for void*, but the program is not any less valid for void*.
I don't know what else to try.

Any help is appreciated, and I am also wondering if there is an overall workflow for working through establishing the proper conditions.  I am looking at the "WP Goals" tab and it is beyond me.  Do the experts learn to read through the WP Goals, or is it more common to add superfluous assertions, or is there some other best practice for working towards provable code?

Thanks,
-Jamie



typedef struct {
    void **content;
    int capacity;
    int count;
} LIST;

/*@predicate listvalid(LIST *list) =
    \valid(list) &&
    list->count >= 0 && list->count <= list->capacity &&
    list->capacity >= 0 && list->capacity <= 1000 &&
    \valid(list->content + (0..list->capacity-1));
*/

/*@requires listvalid(list);
requires \separated(list, list->content);
ensures listvalid(list);
assigns list->content[0..list->capacity-1], list->count;
*/
void AddTail(LIST *list, void *data) {
    //@assert \valid(list->content + (0..list->capacity-1));
    if (list->count >= list->capacity) {
        // strictly-greater is impossible given requirements
        //@assert list->count == list->capacity;
        return;
    }
    //@assert list->count < list->capacity;
    //@assert \valid(list->content + (0..list->capacity-1));
    list->content[list->count] = data;
    //@assert \valid(list->content + (0..list->capacity-1));
    list->count++;
    //@assert \valid(list);
    //@assert list->count >= 0;
    //@assert list->count <= list->capacity;
    //@assert list->capacity >= 0 && list->capacity <= 1000;
    //@assert \valid(list->content + (0..list->capacity-1));
}

:EXTERNAL: :NOTICE: The contents of this communication (whether in physical or electronic form) contains confidential and proprietary information that is the property of Authentix, Inc., its subsidiaries and affiliates, and is not for publication, distribution or dissemination without the express written consent of Authentix, Inc., its subsidiaries and affiliates and is intended for use only by the recipient.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181024/9beb2848/attachment-0001.html>