sig
  type t = Contract_types.contract
  val create : loc:Cil_types.location -> Cil_types.spec -> Contract.t
  val translate_preconditions :
    Cil_types.kernel_function ->
    Cil_types.kinstr -> Env.t -> Contract.t -> Env.t
  val translate_postconditions :
    Cil_types.kernel_function -> Cil_types.kinstr -> Env.t -> Env.t
  val must_translate_ppt_ref : (Property.t -> bool) Stdlib.ref
  val must_translate_ppt_opt_ref : (Property.t option -> bool) Stdlib.ref
end