From f8aadfc2d2e4f2d1fe75959d03d96d65bbb2af24 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 10 Oct 2022 18:26:52 +0200
Subject: [PATCH] [kernel] Abstract ctx type
---
src/kernel_services/analysis/logic_deps.mli | 11 +----------
1 file changed, 1 insertion(+), 10 deletions(-)
diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli
index fd8d20303a0..5470e3dd73d 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
--
GitLab