--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fix for inductive predicate



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