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


  • Subject: [Frama-c-discuss] Having trouble proving a (seemingly) simple program
  • From: Jamie.Kawabata at authentix.com (Jamie Kawabata)
  • Date: Tue, 23 Oct 2018 20:29:03 +0000
  • In-reply-to: <CY4PR08MB2661FB7BCA42E5E63696E4A79DF50@CY4PR08MB2661.namprd08.prod.outlook.com>
  • References: <CY4PR08MB2661FB7BCA42E5E63696E4A79DF50@CY4PR08MB2661.namprd08.prod.outlook.com>

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/20181023/9f84ad72/attachment.html>