--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Dynamically allocated lists



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>