From 1e47176ecc4d995e069f22e9fca09d4cb0818d8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Jul 2023 14:15:56 +0200
Subject: [PATCH] [Eva] Removes unused fold functions from Db.Value.
---
src/kernel_services/plugin_entry_points/db.ml | 12 ------------
src/kernel_services/plugin_entry_points/db.mli | 6 ------
2 files changed, 18 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 6bb0420d424..1da9ccf2e15 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -470,18 +470,6 @@ module Value = struct
Table_By_Callstack.find stmt)
with Not_found -> None
- let fold_stmt_state_callstack f acc ~after stmt =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match get_stmt_state_callstack ~after stmt with
- | None -> acc
- | Some h -> Eva_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
-
- let fold_state_callstack f acc ~after ki =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match ki with
- | Kglobal -> f (globals_state ()) acc
- | Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
-
let is_reachable = Cvalue.Model.is_reachable
exception Is_reachable
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 3386adefaae..3e820ffff2a 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -216,12 +216,6 @@ module Value : sig
(** [after] is false by default.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val fold_stmt_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> stmt -> 'a
-
- val fold_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> kinstr -> 'a
-
(** {3 Reachability} *)
val is_accessible : kinstr -> bool
--
GitLab