Skip to content
Snippets Groups Projects
Commit 42ebe682 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Results: uses function_calls for [is_called], [callers] and [callsites].

parent f6ef864d
No related branches found
No related tags found
No related merge requests found
...@@ -56,6 +56,20 @@ let register_call kinstr kf = ...@@ -56,6 +56,20 @@ let register_call kinstr kf =
let add _kf = Kernel_function.Map.singleton caller callsite in let add _kf = Kernel_function.Map.singleton caller callsite in
ignore (Callers.memo ~change add kf) ignore (Callers.memo ~change add kf)
let is_called = Callers.mem
let callers kf =
try
let calls = Kernel_function.Map.bindings (Callers.find kf) in
List.map fst calls
with Not_found -> []
let callsites kf =
try
let calls = Kernel_function.Map.bindings (Callers.find kf) in
List.map (fun (kf, set) -> kf, StmtSet.elements set) calls
with Not_found -> []
type analysis_target = type analysis_target =
[ `Builtin of string * Builtins.builtin * cacheable * funspec [ `Builtin of string * Builtins.builtin * cacheable * funspec
......
...@@ -36,3 +36,14 @@ type analysis_target = ...@@ -36,3 +36,14 @@ type analysis_target =
Also registers the call in tables for the functions below. *) Also registers the call in tables for the functions below. *)
val define_analysis_target: val define_analysis_target:
?recursion_depth:int -> kinstr -> kernel_function -> analysis_target ?recursion_depth:int -> kinstr -> kernel_function -> analysis_target
(** Returns true if the function has been analyzed. *)
val is_called: kernel_function -> bool
(** Returns the list of inferred callers of the given function. *)
val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
(** Returns the list of inferred callers, and for each of them, the list
of callsites (the call statements) inside. *)
val callsites: kernel_function -> (kernel_function * stmt list) list
...@@ -670,10 +670,6 @@ let is_bottom : type a. a evaluation -> bool = ...@@ -670,10 +670,6 @@ let is_bottom : type a. a evaluation -> bool =
let module L = (val lvaluation : Lvaluation) in let module L = (val lvaluation : Lvaluation) in
L.is_bottom L.v L.is_bottom L.v
let is_called kf =
let module M = Make () in
M.is_reachable (at_start_of kf)
let is_reachable stmt = let is_reachable stmt =
let module M = Make () in let module M = Make () in
M.is_reachable (before stmt) M.is_reachable (before stmt)
...@@ -686,29 +682,9 @@ let condition_truth_value = Db.Value.condition_truth_value ...@@ -686,29 +682,9 @@ let condition_truth_value = Db.Value.condition_truth_value
(* Callers / callsites *) (* Callers / callsites *)
let callers kf = let is_called = Function_calls.is_called
let f = function let callers = Function_calls.callers
| [] | [_] -> None let callsites = Function_calls.callsites
| _ :: (caller,_) :: _-> Some caller
in
at_start_of kf |> callstacks |>
List.filter_map f |> List.sort_uniq Kernel_function.compare
let uniq_sites = List.sort_uniq Cil_datatype.Stmt.compare
let callsites kf =
let module Map = Kernel_function.Map in
let f acc = function
| [] | (_,Cil_types.Kglobal) :: _ -> acc
| [(_,Kstmt _)] -> assert false (* End of callstacks should have no callsite *)
| (_kf,Kstmt stmt) :: (caller,_) :: _ -> (* kf = _kf *)
Map.update caller
(fun old -> Some (stmt :: Option.value ~default:[] old)) acc
in
at_start_of kf |> callstacks |>
List.fold_left f Map.empty |> Map.to_seq |> List.of_seq |>
List.map (fun (kf,sites) -> kf, uniq_sites sites)
(* Result conversion *) (* Result conversion *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment