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

[Eva] api: Add results folding by callstack

parent 3e7b37ff
No related branches found
No related tags found
No related merge requests found
...@@ -159,8 +159,16 @@ struct ...@@ -159,8 +159,16 @@ struct
(* Accessors *) (* Accessors *)
let callstacks : ('a, restricted_to_callstack) t -> callstack list = function let callstacks : ('a, restricted_to_callstack) t -> callstack list = function
| ByCallstack l -> List.map fst l
| 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
(* Fold *)
let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) :
('a, restricted_to_callstack) t -> 'b =
function
| Top | Bottom -> acc (* What else to do when Top is given ? *)
| ByCallstack l -> List.fold_left (fun acc (cs,x) -> f cs x acc) acc l
(* Map *) (* Map *)
...@@ -255,7 +263,19 @@ struct ...@@ -255,7 +263,19 @@ struct
| `Value v -> Result.ok v | `Value v -> Result.ok v
let callstacks req = let callstacks req =
Response.callstacks (get_by_callstack req) get_by_callstack req |> Response.callstacks
let fold_callstacks f acc req =
let f' cs _res acc =
f cs (in_callstack cs req) acc
in
get_by_callstack req |> Response.fold f' acc
let by_callstack req =
let f cs _res acc =
(cs, in_callstack cs req) :: acc
in
get_by_callstack req |> Response.fold f []
let is_reachable req = let is_reachable req =
match get req with match get req with
...@@ -428,12 +448,23 @@ struct ...@@ -428,12 +448,23 @@ struct
end end
(* State requests *) (* Working with callstacks *)
let callstacks req = let callstacks req =
let module E = Make () in let module E = Make () in
E.callstacks req E.callstacks req
let fold_callstacks f acc req =
let module E = Make () in
E.fold_callstacks f acc req
let by_callstack req =
let module E = Make () in
E.by_callstack req
(* State requests *)
let equality_class exp req = let equality_class exp req =
let module E = Make () in let module E = Make () in
E.equality_class exp req E.equality_class exp req
...@@ -442,6 +473,7 @@ let as_cvalue_model req = ...@@ -442,6 +473,7 @@ let as_cvalue_model req =
let module E = Make () in let module E = Make () in
E.as_cvalue_model req E.as_cvalue_model req
(* Evaluation *) (* Evaluation *)
module type Evaluator = module type Evaluator =
......
...@@ -53,8 +53,12 @@ val in_callstack : callstack -> request -> request ...@@ -53,8 +53,12 @@ val in_callstack : callstack -> request -> request
val in_callstacks : callstack list -> request -> request val in_callstacks : callstack list -> request -> request
val filter_callstack : (callstack -> bool) -> request -> request val filter_callstack : (callstack -> bool) -> request -> request
(* State requests *) (* 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
(* 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
val as_cvalue_model : request -> Cvalue.Model.t result val as_cvalue_model : request -> Cvalue.Model.t result
......
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