diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli index fd8d20303a0aa5856209ad14f7fc04e0374cfeb4..5470e3dd73d5b8ca541444b39215d255d0d43eb0 100644 --- a/src/kernel_services/analysis/logic_deps.mli +++ b/src/kernel_services/analysis/logic_deps.mli @@ -24,16 +24,7 @@ open Cil_types val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref -type ctx = { - site: ctx_site; - before: bool option; - kf: Kernel_function.t -} - -and ctx_site = - | FunctionContract - | StatementContract of stmt - | StatementAnnotation of stmt +type ctx val mk_ctx_func_contrat: ?before:bool -> kernel_function -> ctx (** To build an interpretation context relative to function