--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2018 ---
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>