--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on February 2012 ---
Hi, I'm a bit surprised with this "bug" from programatic invokation of Wp. The GUI plug-in for WP simply invokes the function "Wp.wp_compute" as I you do programmatically. Actually, the consolidated status for properties that depend on others is performed by the Frama-C kernel, not by Wp. However, the GUI plug-in for WP explicitly ask the GUI for refreshing, which may cause property statuses to be re-computed : /* from src/wp/wp_gui.ml */ let run_and_prove (main_ui:Design.main_window_extension_points) strategy = [.....] Register.wp_compute s.sp_kf s.sp_bhv s.sp_ip [......] main_ui#rehighlight () ; [.....] Have also a look at module Property_status for forcing the kernel to recompute consolidation : Property_status.Feedback.get : Property.t -> t (* feedback used for bullets *) Property_status.Consolidation.get : Property.t -> Consolidation.t (* full consolidation data *) Regards, L.