diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml index 2b3bf770836f8811c703577bf9718b627a456c4c..be5eb41d5d1c6f1f542cf27a213372c95b6037d5 100644 --- a/src/plugins/constant_propagation/api.ml +++ b/src/plugins/constant_propagation/api.ml @@ -135,8 +135,7 @@ class propagate project fnames ~cast_intro = object(self) | None -> raise Cannot_change | Some s -> s in - let evaled = Eva.Results.( - before stmt |> eval_exp expr |> as_cvalue |> default Cvalue.V.top) in + let evaled = Eva.Results.(before stmt |> eval_exp expr |> as_cvalue) in let b, m = Cvalue.V.find_lonely_binding evaled in let can_replace vi = (* can replace the current expr by [vi] iff (1) it is a source var, or diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index af26fe2d1f894f8b9da96a68438fa6abcacdf519..b694d6d85ecb58b9256b6e05dcbf66547377dfa3 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -82,8 +82,7 @@ struct Result.value ~default:[] let to_cvalue kinstr lval = - before_kinstr kinstr |> eval_lval lval |> as_cvalue |> - Result.value ~default:Cvalue.V.bottom + before_kinstr kinstr |> eval_lval lval |> as_cvalue let to_location kinstr lval = before_kinstr kinstr |> eval_address lval |> as_location |> diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 6e4c7a769a406bfbe3294324b09f2a09c525ed86..58006b2c451753ca0a1707acada914bcd5106ac6 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -228,8 +228,12 @@ module Results: sig (** Converts the value into a floating point abstraction. *) val as_fval : value evaluation -> Fval.t result + (** Converts the value into a Cvalue abstraction. Converts error cases + into bottom and top values accordingly. *) + val as_cvalue : value evaluation -> Cvalue.V.t + (** Converts the value into a Cvalue abstraction. *) - val as_cvalue : value evaluation -> Cvalue.V.t result + val as_cvalue_result : value evaluation -> Cvalue.V.t result (** Converts into a C location abstraction. *) diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index c61dbb8f510a0b0f2f0d6a9131f05c81ab433108..87a2ee9758f3ede02bd347959d77a58f4da61270 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -553,13 +553,19 @@ let callee stmt = (* Value conversion *) -let as_cvalue (Value evaluation) = +let as_cvalue_result (Value evaluation) = let module E = (val evaluation : Evaluation) in E.as_cvalue E.v +let as_cvalue evaluation = + match as_cvalue_result evaluation with + | Ok v -> v + | Error Bottom -> Cvalue.V.bottom + | Error (Top | DisabledDomain) -> Cvalue.V.top + let as_ival evaluation = try - Result.map Cvalue.V.project_ival (as_cvalue evaluation) + Result.map Cvalue.V.project_ival (as_cvalue_result evaluation) with Cvalue.V.Not_based_on_null -> Result.error Top diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index 53251203bb127ca102b24ed9fce2253ef10c27f4..e24441ccb68a3473d768a8129ee28eb45eb12fe0 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -216,8 +216,12 @@ val as_ival : value evaluation -> Ival.t result (** Converts the value into a floating point abstraction. *) val as_fval : value evaluation -> Fval.t result +(** Converts the value into a Cvalue abstraction. Converts error cases + into bottom and top values accordingly. *) +val as_cvalue : value evaluation -> Cvalue.V.t + (** Converts the value into a Cvalue abstraction. *) -val as_cvalue : value evaluation -> Cvalue.V.t result +val as_cvalue_result : value evaluation -> Cvalue.V.t result (** Converts into a C location abstraction. *)