--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to specify the options when calling wp_compute?



Hi,

   I have specified the options already. I used the version-Carbon before
and the way you said is not supported. Now I move my work to  Nitrogen and
it works.
   I find a small problem. If wp plugin is loaded as follow:

let module OLS = Datatype.Option(Datatype.List(Datatype.String)) in
let module OKF = Datatype.Option(Kernel_function) in
        let module OP = Datatype.Option(Property) in
        let wp_compute = Dynamic.get ~plugin:"Wp" "wp_compute" (Datatype.func3
OKF.ty OLS.ty OP.ty Datatype.unit) in
        wp_compute (Some(kf)) bhv (Some(ip)); and the type of bhv is:
string list option When the value of bhv as None(another case is not
tested), it will raise an exception ,described as follow: Unexpected error
(Type.Make_tbl(Key)(Info).Incompatible_type("Wp.wp_compute has type
Cil_datatype.Kf.t option -> string list -> identified property option ->
unit but is used with type Cil_datatype.Kf.t option -> string list option
-> identified property option -> unit.")). I wonder how it is. Thank you
for your kindness.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111103/79aa8cfc/attachment.htm>