--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2013 ---
Thanks Nicolas for the post. Indeed, it is the correct fix. Actually, there is also a missing frame, and the complete fix is provided in attachment. Regards, L. -------------- next part -------------- A non-text attachment was scrubbed... Name: fixpoint.patch Type: application/octet-stream Size: 1563 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130528/83223fe3/attachment.obj> -------------- next part -------------- Le 25 mai 2013 ? 03:11, Nicolas Marti a ?crit : > Dear all, > > I always had issues with the code generation for inductive definition in Frama-c (for instance when defining linked lists). > Sometime it happens that the inductive predicate type is not generalized enough regarding all its constructors > Maybe some of you had the same issue, so here is a simple fix (though still no inductive code production or why3): > > in file src/wp/LogicCompiler, > in function compile_lbinduction > > around the comment (* Re-compile final cases *) > put the two following lines: > > Definitions.update_symbol ldef ; > Signature.update l (SIG sigm) ; > > this should fix the issue. > > Regards, > > Nicolas > _______________________________________________ > 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