--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2009 ---
[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



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