module E_ACSL:sig
..end
val generate_code : string -> Project.t
Dynamic.get ~plugin:"E_ACSL" "generate_code" (Datatype.func Datatype.string Project.ty)
val predicate_to_exp : Cil_datatype.Kf.t -> Cil_datatype.Predicate.t -> Cil_datatype.Exp.t
Dynamic.get ~plugin:"E_ACSL" "predicate_to_exp" (Datatype.func Kernel_function.ty (Datatype.func Cil_datatype.Predicate.ty Cil_datatype.Exp.ty))