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