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