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] Problem on Plugin development with WP plugin

  • Subject: [Frama-c-discuss] Problem on Plugin development with WP plugin
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Fri, 1 Nov 2013 20:01:37 +0000
Dear all,

Is there anybody who used the api of frama-c dynamic plugins before?

Here i have a problem on using the api of Wp dynamic plugin:

This is an example interface of the Dynamic_plugins.Wp.Wpo :

val iter_on_goals : (po -> unit) -> unit
Access it by Dynamic.get ~plugin:"Wp.Wpo" "iter_on_goals"
(Datatype.func (Datatype.func Wpo.ty Datatype.unit) Datatype.unit)

while i accessing this interface by using:

let iter_on_goals =
    Dynamic.get ~plugin:"Wp.Wpo" "iter_on_goals" (Datatype.func
(Datatype.func Wpo.ty Datatype.unit) Datatype.unit)
in


Then, I compiled my plugin with make, an Error came with:
"Error: Unbound module Wpo"

I couldn't open the Wpo module like open other frama-c kernel
modules(e.g. Db moudle and Cil_types module). So i don't know how to
fix this problem.

Any suggestion on using these dynamic frama-c apis?

Thank you very much and looking forward to hearing from you.

Best regards,
-Yibiao