diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 6bb0420d424051183dee97be4a4269f472144429..1da9ccf2e15d1e4cc7265d5ca0a464811ce1d474 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 3386adefaaeb8ba789d257a5ca2dda4baca9c1d7..3e820ffff2a188f6965eade123baf0f20a01d628 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