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