Skip to content
Snippets Groups Projects
Commit ecb85004 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] api: Add iter_callstacks and is_empty

parent 9e84c9a8
No related branches found
No related tags found
No related merge requests found
...@@ -43,8 +43,9 @@ module Results: sig ...@@ -43,8 +43,9 @@ module Results: sig
(* Working with callstacks *) (* Working with callstacks *)
val callstacks : request -> callstack list val callstacks : request -> callstack list
val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
val by_callstack : request -> (callstack * request) list val by_callstack : request -> (callstack * request) list
val iter_callstacks : (callstack -> request -> unit) -> request -> unit
val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
(* State requests *) (* State requests *)
val equality_class : Cil_types.exp -> request -> Cil_types.exp list result val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
...@@ -75,6 +76,7 @@ module Results: sig ...@@ -75,6 +76,7 @@ module Results: sig
val alarms : 'a evaluation -> Alarms.t list val alarms : 'a evaluation -> Alarms.t list
(* Reachability *) (* Reachability *)
val is_empty : request -> bool
val is_bottom : 'a evaluation -> bool val is_bottom : 'a evaluation -> bool
val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *) 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 *) val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
......
...@@ -173,6 +173,14 @@ struct ...@@ -173,6 +173,14 @@ struct
| Top | Bottom -> [] (* What else to do when Top is given ? *) | Top | Bottom -> [] (* What else to do when Top is given ? *)
| ByCallstack l -> List.map fst l | ByCallstack l -> List.map fst l
(* Iter *)
let iter (f : callstack -> 'a -> unit) :
('a, restricted_to_callstack) t -> unit =
function
| Top | Bottom -> () (* What else to do when Top is given ? *)
| ByCallstack l -> List.iter (fun (cs,x) -> f cs x) l
(* Fold *) (* Fold *)
let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) : let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) :
...@@ -290,6 +298,12 @@ struct ...@@ -290,6 +298,12 @@ struct
let callstacks req = let callstacks req =
get_by_callstack req |> Response.callstacks get_by_callstack req |> Response.callstacks
let iter_callstacks f req =
let f' cs _res =
f cs (in_callstack cs req)
in
get_by_callstack req |> Response.iter f'
let fold_callstacks f acc req = let fold_callstacks f acc req =
let f' cs _res acc = let f' cs _res acc =
f cs (in_callstack cs req) acc f cs (in_callstack cs req) acc
...@@ -481,6 +495,10 @@ let callstacks req = ...@@ -481,6 +495,10 @@ let callstacks req =
let module E = Make () in let module E = Make () in
E.callstacks req E.callstacks req
let iter_callstacks f acc =
let module E = Make () in
E.iter_callstacks f acc
let fold_callstacks f acc req = let fold_callstacks f acc req =
let module E = Make () in let module E = Make () in
E.fold_callstacks f acc req E.fold_callstacks f acc req
...@@ -636,6 +654,10 @@ let alarms : type a. a evaluation -> Alarms.t list = ...@@ -636,6 +654,10 @@ let alarms : type a. a evaluation -> Alarms.t list =
(* Reachability *) (* Reachability *)
let is_empty rq =
let module E = Make () in
E.callstacks rq = []
let is_bottom : type a. a evaluation -> bool = let is_bottom : type a. a evaluation -> bool =
function function
| Value evaluation -> | Value evaluation ->
......
...@@ -63,8 +63,9 @@ val filter_callstack : (callstack -> bool) -> request -> request ...@@ -63,8 +63,9 @@ val filter_callstack : (callstack -> bool) -> request -> request
(* Working with callstacks *) (* Working with callstacks *)
val callstacks : request -> callstack list val callstacks : request -> callstack list
val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
val by_callstack : request -> (callstack * request) list val by_callstack : request -> (callstack * request) list
val iter_callstacks : (callstack -> request -> unit) -> request -> unit
val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
(* State requests *) (* State requests *)
val equality_class : Cil_types.exp -> request -> Cil_types.exp list result val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
...@@ -95,6 +96,7 @@ val is_initialized : value evaluation -> bool ...@@ -95,6 +96,7 @@ val is_initialized : value evaluation -> bool
val alarms : 'a evaluation -> Alarms.t list val alarms : 'a evaluation -> Alarms.t list
(* Reachability *) (* Reachability *)
val is_empty : request -> bool
val is_bottom : 'a evaluation -> bool val is_bottom : 'a evaluation -> bool
val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *) 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 *) val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
......
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