--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2013 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130525/17c3c0a6/attachment.html>