--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to get the "VALID" results with dynamically calling wp?



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.