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