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

Hi,
So many topics in this message ;-)

WP & Inductive : we only generate the lemma corresponding to the different induction cases, as ways to establish the predicate.
The inversion / induction lemma is not generated, because SMT solvers will instantiate them infinitely often...

WP & Allocation : there is no built-in support for allocation and freshness. You must simulate these properties by hand by using dedicated mallocs and several tricks.
The most prominent problem is to deal with separation efficiently.

Predicate with pointers : you absolutely need framing properties. Assuming a predicate is true at program point L, is-it still true after writing through some pointer ?
Those kind of problems are known to be very difficult in the literature? This is certainly a hot spot for deductive reasoning in general.

L.

Le 16 janv. 2015 ? 15:53, Filip Niksic <fniksic at mpi-sws.org> a ?crit :

> 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
> 
> <list.c>_______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss