sig
type t = Contract_types.contract
val create : loc:Cil_types.location -> Cil_types.spec -> Contract.t
val translate_preconditions :
Cil_types.kernel_function -> Env.t -> Contract.t -> Env.t
val translate_postconditions : Cil_types.kernel_function -> Env.t -> Env.t
end