From 12e98c22ae930d3587e1d08b15dd83629c2f96c9 Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Wed, 29 Sep 2021 17:49:22 +0200 Subject: [PATCH] [Eva] api: Add callers and callsites requests --- src/plugins/value/Eva.mli | 6 +++++- src/plugins/value/utils/results.ml | 20 +++++++++++++++++++- src/plugins/value/utils/results.mli | 6 +++++- 3 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 7162412e2f9..b645bda7774 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -72,11 +72,15 @@ module Results: sig val is_initialized : evaluation -> bool val alarms : evaluation -> Alarms.t list - (* Bottomness *) + (* Reachability *) val is_bottom : evaluation -> bool val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *) val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *) + (* Callers / callsites *) + val callers : Cil_types.kernel_function -> Cil_types.kernel_function list + val callsites : Cil_types.kernel_function -> Cil_types.stmt list + end module Value_results: sig diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index 48189f931d4..c43d6d4ca75 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -631,7 +631,7 @@ let alarms evaluation = let module E = (val evaluation : Evaluation) in E.alarms E.v -(* Bottomness *) +(* Reachability *) let is_bottom evaluation = let module E = (val evaluation : Evaluation) in @@ -644,3 +644,21 @@ let is_called kf = let is_reachable stmt = let module M = Make () in M.is_reachable (before stmt) + +(* Callers / callsites *) + +let callers kf = + let f = function + | [] | [_] -> None + | _ :: (kf,_) :: _-> Some kf + in + at_start_of kf |> callstacks |> + List.filter_map f |> List.sort_uniq Kernel_function.compare + +let callsites kf = + let f = function + | [] | (_,Cil_types.Kglobal) :: _ -> None + | (_,Kstmt stmt) :: _-> Some stmt + in + at_start_of kf |> callstacks |> + List.filter_map f |> List.sort_uniq Cil_datatype.Stmt.compare diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index 17fb9dda5a7..1d53fa4addd 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -92,9 +92,13 @@ val as_zone : lvaluation -> Locations.Zone.t result val is_initialized : evaluation -> bool val alarms : evaluation -> Alarms.t list -(* Bottomness *) +(* Reachability *) val is_bottom : evaluation -> bool val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *) val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *) +(* Callers / callsites *) +val callers : Cil_types.kernel_function -> Cil_types.kernel_function list +val callsites : Cil_types.kernel_function -> Cil_types.stmt list + [@@@ api_end] -- GitLab