--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on February 2012 ---
Hello, On 02/15/2012 01:18 PM, Henry wrote: > I wonder how to make it with > OCaml code in my own program, not by command line. For that if it calls > Wp.wp_compute only one property can be proved once. Hope it's clear for you. Here is a script which does what you want: === run_wp.ml === let main () = Dynamic.Parameter.Bool.on "-wp" (); Dynamic.get ~plugin:"Wp" "run" (Datatype.func Datatype.unit Datatype.unit) () let () = Db.Main.extend main ========== $ frama-c-gui -load-script run_wp test.i If test.i is your original example, all the properties are valid. One additional remark: if you remove the call to Dynamic.get in this code, it is possible to observe the same behavior, but it is only by chance: it is not specified that the main of this script is executed before the main of the WP plug-in which looks at the value of -wp in order to run the WP calculus. Hence the second function which forces the execution of WP after setting -wp. Hope this helps, Julien