Module Dynamic_plugins.Wp

module Wp: sig .. end

module Wpo: sig .. end
val wp_compute_kf : Cil_datatype.Kf.t option -> string list -> string list -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_compute_kf" (Datatype.func (Datatype.option Kernel_function.ty) (Datatype.func (Datatype.list Datatype.string) (Datatype.func (Datatype.list Datatype.string) Datatype.unit)))
val wp_clear_session : unit -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_clear_session" (Datatype.func Datatype.unit Datatype.unit)
val wp_iter_session : (Wpo.po -> unit) -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_iter_session" (Datatype.func (Datatype.func Wpo.ty Datatype.unit) Datatype.unit)
val wp_compute : Cil_datatype.Kf.t option -> string list -> Property.t option -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_compute" (Datatype.func (Datatype.option Kernel_function.ty) (Datatype.func (Datatype.list Datatype.string) (Datatype.func (Datatype.option Property.ty) Datatype.unit)))
val wp_end_session : unit -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_end_session" (Datatype.func Datatype.unit Datatype.unit)
val wp_compute_call : Cil_datatype.Stmt.t -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_compute_call" (Datatype.func Cil_datatype.Stmt.ty Datatype.unit)
val run : unit -> unit
Access it by Dynamic.get ~plugin:"Wp" "run" (Datatype.func Datatype.unit Datatype.unit)
val wp_clear : unit -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_clear" (Datatype.func Datatype.unit Datatype.unit)
val wp_begin_session : unit -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_begin_session" (Datatype.func Datatype.unit Datatype.unit)
val wp_compute_ip : Property.t -> unit
Access it by Dynamic.get ~plugin:"Wp" "wp_compute_ip" (Datatype.func Property.ty Datatype.unit)