--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2011 ---
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>