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

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.
>
> _______________________________________________
> 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/20181024/5b603ceb/attachment-0001.html>