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: Mon, 13 Jul 2009 08:18:47 +0200
I tried to port to Beryllium the patch provided by Pascal Cuoq here:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-January/000892.html (with this patch you can access the several states attached to a statement while the analysis is taking place).

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). It's something
that've changed between Lithium and Beryllium and it's independent from
this patch.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: frama-c-20090601_beta1-states_hook.patch
Type: text/x-patch
Size: 3890 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090713/6bff4eab/attachment.bin