--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2015 ---
Hi all, I am trying to understand how to use Frama-C to reason about dynamically allocated lists. In the attached code, I have a global list pointed to by a global pointer r, and a function add_node that allocates a new node and adds it as a new head of the list. I have defined an inductive predicate reachable to reason about reachability, and now I want to prove that the function add_node maintains the invariant that the list does not contain a cycle: /*@ requires reachable(r, \null); @ assigns r; @ ensures reachable(r, \null); @*/ void add_node() { struct node *new = malloc(sizeof(struct node)); if (new != NULL) { new->next = r; r = new; } } I am trying to verify this using Jessie, as WP cannot deal with dynamic memory allocation. I am also using libc headers with ACSL specification that come with Frama-C. $ frama-c -jessie -cpp-extra-args="-I $(frama-c -print-path)/libc -nostdinc" list.c However, the generated verification conditions cannot be verified, at least not with Z3 of Alt-Ergo. It seems that malloc somehow messes the fact that \null is reachable from r. Does anyone know what the problem is and how to solve it? As a side question, what are the limitations of WP when handling inductive predicates? As far as I can see, it completely eliminates the fact that they are "inductive", and produces just plain predicates. It doesn't give anything that resembles the corresponding induction principles. Thanks, Filip -------------- next part -------------- A non-text attachment was scrubbed... Name: list.c Type: text/x-csrc Size: 679 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150116/32359fe0/attachment.c>