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] [Values] patch to access the several states attached to a statement

  • Subject: [Frama-c-discuss] [Values] patch to access the several states attached to a statement
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Tue, 14 Jul 2009 05:30:40 +0200
  • In-reply-to: <5EFD4D7AC6265F4D9D3A849CEA9219191AB1E9@LAXA.intra.cea.fr>
  • References: <1247465927.3378.26.camel@residence.localdomain> <5EFD4D7AC6265F4D9D3A849CEA9219191AB1E8@LAXA.intra.cea.fr> <5EFD4D7AC6265F4D9D3A849CEA9219191AB1E9@LAXA.intra.cea.fr>
On Mon, 2009-07-13 at 14:59 +0200, CUOQ Pascal wrote:
> > It compiles fine and can be used in a plug-in, but doesn't work quite
> > well. From a quick debug, it seems that in 'let merge_current'
> > Db.Value.Record_Value_Callbacks is always empty (and therefore
> > Record_Value_Superposition callbacks are not called).
> 
> In your patch (and therefore your modified version)
> I am quite sure that the if that comes just before
> "let current_superpositions = ..." should be
> "(not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ()))"
> and not "if not (Db.Value.Record_Value_Callbacks.is_empty ())"
> as it is currently.

Well I thought of that, but only because the logical structure of the
code was kinda weird: if (cond1) code1; if (cond1) code2;
However, since the code was identical in Lithium and actually worked, I
wasn't sure it was the proper way to fix this.

Anyway, I confirm it fixes the problem, so here is attached the fixed
patch.

> Thanks for the patches, we should have no problem integrating
> them although we may need to alter the documentation
> accordingly. Normally, all sections in the code marked
> with a "@plugin development guide" comment can not be changed
> without making sure that the plug-in development guide is
> updated (and that may be refined for the future if each plug-in
> starts to have its own "programmatic documentation").

I will try to provide a patch for the documentation as well.

> Best regards, and happy festivities where applicable.

Thanks ! You too ^_^
-------------- next part --------------
A non-text attachment was scrubbed...
Name: frama-c-20090601_beta1-states_hook.patch
Type: text/x-patch
Size: 3904 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090714/5735c495/attachment.bin