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] Dynamically allocated lists

  • Subject: [Frama-c-discuss] Dynamically allocated lists
  • From: fniksic at mpi-sws.org (Filip Niksic)
  • Date: Fri, 16 Jan 2015 15:53:30 +0100
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>