Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] How to get the "VALID" results with dynamically calling wp?
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 15 Feb 2012 14:48:33 +0100
  • In-reply-to: <CALiiei6L0SA3qUph+P7ghssfZozbsg-ygJvvk=mmDHk_OnhMXw@mail.gmail.com>
  • References: <CALiiei43n6f68tBKXE4sc6fA_0N5=dxsj6A1Fc8bEXB+aKSiSw@mail.gmail.com> <CALiiei6L0SA3qUph+P7ghssfZozbsg-ygJvvk=mmDHk_OnhMXw@mail.gmail.com>
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