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>