--- layout: fc_discuss_archives title: Message 62 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?



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