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] How to get the results after running WP within my own plugin?

  • Subject: [Frama-c-discuss] How to get the results after running WP within my own plugin?
  • From: virgile.prevosto at cea.fr (Virgile)
  • Date: Wed, 21 Sep 2011 15:31:48 +0200
  • In-reply-to: <CALiiei6Fq3pTr_FC4opJobZeB=3uvA9GYH-j-zY0XHnHC=tb8Q@mail.gmail.com>
  • References: <CALiiei6Fq3pTr_FC4opJobZeB=3uvA9GYH-j-zY0XHnHC=tb8Q@mail.gmail.com>
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