--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on September 2011 ---
[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?



Hi,

   Now my plugin uses the Plug-in Developer Interface of WP as below:


let prove_prop (kf:Db_types.kernel_function) (bhv:string list option) prop=
let module OLS = Datatype.Option(Datatype.List(Datatype.String)) in
let module OKF = Datatype.Option(Kernel_function) in
let module OP = Datatype.Option(Property) in
let wp_compute = Dynamic.get ~plugin:"Wp" "wp_compute" (Datatype.func3
OKF.ty OLS.ty OP.ty Datatype.unit) in
wp_compute (Some(kf)) bhv prop


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.


Best Wishes.

Henry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110921/57ade7b1/attachment.htm>