--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on September 2011 ---
On 21/09/2011 15:06, ??? wrote: > Now it can print out the results such as > > [wp] [WP:simplified] Goal store_equal_assert_48 : Valid > > But, how can I get the result as a return value in my program so I can > do further work according to the value. Hope you can help me. > Hello, If I understand well what you are doing, you have managed to launch WP from your plugin and you would like to get back the status it has computed for each ACSL annotation of the program. This is managed by the Properties_status module (src/logic/properties_status.ml) in Frama-C Carbon. This module aggregates all information about the validity of ACSL properties (Any plugin that can tell if a given property is valid or invalid is supposed to register this fact in Properties_status, not just the WP plugin). Note however that this part of Frama-C is currently under heavy refactoring (in order to provide more accurate results when aggregating status coming from various distinct analyses) and that Nitrogen will provide a brand new interface for that, mostly incompatible with the current one. Hope this helps, -- E tutto per oggi, a la prossima volta Virgile