diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 3187131ce956618f61741074039124ac9d663f88..1c4b9b634e0cdd9ea1211a770d700d4c8186835e 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -43,8 +43,9 @@ module Results: sig (* Working with callstacks *) val callstacks : request -> callstack list - val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a 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 *) val equality_class : Cil_types.exp -> request -> Cil_types.exp list result @@ -75,6 +76,7 @@ module Results: sig val alarms : 'a evaluation -> Alarms.t list (* Reachability *) + val is_empty : request -> 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_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *) diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index 9ace1a390c064a4a0c4fa166f5f29a268439c2ac..40c3097ace67488459b6438a9ae62376ac54aec0 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -173,6 +173,14 @@ struct | Top | Bottom -> [] (* What else to do when Top is given ? *) | 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 *) let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) : @@ -290,6 +298,12 @@ struct let callstacks req = 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 f' cs _res acc = f cs (in_callstack cs req) acc @@ -481,6 +495,10 @@ let callstacks req = let module E = Make () in 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 module E = Make () in E.fold_callstacks f acc req @@ -636,6 +654,10 @@ let alarms : type a. a evaluation -> Alarms.t list = (* Reachability *) +let is_empty rq = + let module E = Make () in + E.callstacks rq = [] + let is_bottom : type a. a evaluation -> bool = function | Value evaluation -> diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index 4afb89e722afd49817c1e5356d3c41ffad677fe0..051d79b605a8185b5706d82325ee0291c0c59cd2 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -63,8 +63,9 @@ val filter_callstack : (callstack -> bool) -> request -> request (* Working with callstacks *) val callstacks : request -> callstack list -val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a 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 *) val equality_class : Cil_types.exp -> request -> Cil_types.exp list result @@ -95,6 +96,7 @@ val is_initialized : value evaluation -> bool val alarms : 'a evaluation -> Alarms.t list (* Reachability *) +val is_empty : request -> 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_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)