diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml index 6149217b42656f40c3f8a06a83d29b9b9a743e4b..afefe850a77fd9b305b979a6f606a52578260c5b 100644 --- a/src/plugins/value/engine/function_calls.ml +++ b/src/plugins/value/engine/function_calls.ml @@ -56,6 +56,20 @@ let register_call kinstr kf = let add _kf = Kernel_function.Map.singleton caller callsite in 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 = [ `Builtin of string * Builtins.builtin * cacheable * funspec diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli index 7a9cfcdc4fc9729779f712640dda15d724c3af58..49bd5a338f7907491558a964a0c6ae57dfb09cbb 100644 --- a/src/plugins/value/engine/function_calls.mli +++ b/src/plugins/value/engine/function_calls.mli @@ -36,3 +36,14 @@ type analysis_target = Also registers the call in tables for the functions below. *) val define_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 diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index 6e92b4373d7234f4919ff260b91e34f67b68df90..7b8666ac8cf7da40e9e6d920128d898269bcea90 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -670,10 +670,6 @@ let is_bottom : type a. a evaluation -> bool = let module L = (val lvaluation : Lvaluation) in 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 module M = Make () in M.is_reachable (before stmt) @@ -686,29 +682,9 @@ let condition_truth_value = Db.Value.condition_truth_value (* Callers / callsites *) -let callers kf = - let f = function - | [] | [_] -> None - | _ :: (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) - +let is_called = Function_calls.is_called +let callers = Function_calls.callers +let callsites = Function_calls.callsites (* Result conversion *)