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

On 01/19/2015 10:39 AM, Lo?c Correnson wrote:
> Hi,
> So many topics in this message ;-)

Unfortunately, as soon as one tries to tackle an example with some 
memory allocation and inductive data structures, a large number of 
difficulties seems to arise.

> 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...

I see, and it makes sense. But when you target Why3, wouldn't it make 
sense to simply generate the inductive predicate (supported in the Why3 
language with the keyword inductive), and let Why3 worry about the 
actual axioms for SMT solvers? Also, shouldn't there be a way to guide 
the SMT solver using triggers?

> 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.

Is there some online resource, like a blog or a stackoverflow post, 
where one could learn a few of these tricks? I've been hacking my way 
around the lack of support for allocation for a while now, and it would 
be really helpful if I wouldn't have to rediscover things on my own.

On the other hand, what is the status of WP regarding allocation? Is 
there a chance we could see this supported in the next release? If not, 
how much work do you think is needed to implement this stuff? Is it 
perhaps something a masters student would be able to do it in a few 
weeks or months? Or would it make for a PhD research project?

> 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.

It is actually surprising that there's such a large body of work on 
separation, and yet it seems that very little of it is made usable in 
practical tools.

Filip