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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Tue, 28 May 2013 15:22:16 +0200
  • In-reply-to: <CALEyfUkLgXGg=pdT0ZXL-D3mxcS38VzsVNcGdHEY8HybgWJK=w@mail.gmail.com>
  • References: <CALEyfUkLgXGg=pdT0ZXL-D3mxcS38VzsVNcGdHEY8HybgWJK=w@mail.gmail.com>
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