From a0d331fd5821298f7e5b98e82ba7dd755d51b0cc Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 3 Jan 2022 17:12:08 +0100
Subject: [PATCH] [Eva] api: Add a result conversion helper
---
src/plugins/value/Eva.mli | 8 +++++++-
src/plugins/value/utils/results.ml | 6 ++++++
src/plugins/value/utils/results.mli | 8 +++++++-
3 files changed, 20 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index ea31e6b674f..4a483f2b21d 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -20,7 +20,7 @@ end
module Results: sig
(* Usage sketch :
- Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int)
+ Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int |> value ~default:0)
or, if you prefer
@@ -124,6 +124,12 @@ module Results: sig
Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
instruction or a [Local_init] with [ConsInit] initializer. *)
val callee : Cil_types.stmt -> Kernel_function.t list
+
+ (* Result conversion *)
+ (** [default d r] extract the value of r if r is Ok or use the default value d
+ otherwise.
+ Equivalent to [Result.value ~default:d r] *)
+ val default : 'a -> 'a result -> 'a
end
module Value_results: sig
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index ff6b6aa67c5..dbb120d24ad 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -756,3 +756,9 @@ let callsites kf =
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 *)
+
+let default default_value result =
+ Result.value ~default:default_value result
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index f4782eacf16..6db2025dfb7 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -23,7 +23,7 @@
[@@@ api_start]
(* Usage sketch :
- Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int)
+ Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int |> value ~default:0)
or, if you prefer
@@ -127,4 +127,10 @@ val callsites : Cil_types.kernel_function ->
Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
instruction or a [Local_init] with [ConsInit] initializer. *)
val callee : Cil_types.stmt -> Kernel_function.t list
+
+(* Result conversion *)
+(** [default d r] extract the value of r if r is Ok or use the default value d
+ otherwise.
+ Equivalent to [Result.value ~default:d r] *)
+val default : 'a -> 'a result -> 'a
[@@@ api_end]
--
GitLab