diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index ea31e6b674f273b1b7856a42b704cd56548987cc..4a483f2b21da19ebd669daf94c90b3680b8b9160 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 ff6b6aa67c5302dd68493f8267ae9be20a273f45..dbb120d24ad96005901ae798bb1b080f27fd3411 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 f4782eacf168dd08183dd9d0a287f9f191d7d47e..6db2025dfb7069d2444edb3a8cfa1fb88247a374 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]