--- layout: fc_discuss_archives title: Message 31 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



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>