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] Fix for inductive predicate
- Subject: [Frama-c-discuss] Fix for inductive predicate
- From: nicolas.marti.japon at gmail.com (Nicolas Marti)
- Date: Sat, 25 May 2013 10:11:29 +0900
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>
- Follow-Ups:
- [Frama-c-discuss] Fix for inductive predicate
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] Fix for inductive predicate
- Prev by Date: [Frama-c-discuss] Bug-fixed release: Fluorine 2
- Next by Date: [Frama-c-discuss] [Value Analysis] Interval Division
- Previous by thread: [Frama-c-discuss] Bug-fixed release: Fluorine 2
- Next by thread: [Frama-c-discuss] Fix for inductive predicate
- Index(es):