diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 7162412e2f9847ccc2bfc14236e81e051e4a53f1..b645bda7774be02b3760a4d427deb25854a870d6 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 48189f931d4081a249f44e57afe39c9e4404d39f..c43d6d4ca7596fad18fa9266fa80a90b10493844 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 17fb9dda5a70d29b49222119d56661316a089d6d..1d53fa4addd21eac337f5b8cd7ac8ff8a4e6fa7f 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]