--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2015 ---
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