From 78886523334196dbaa3a923593bf641ac0c4546e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Tue, 3 Dec 2024 14:54:21 +0100 Subject: [PATCH] [eva] use fold-result --- src/plugins/eva/utils/export.ml | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/src/plugins/eva/utils/export.ml b/src/plugins/eva/utils/export.ml index 4e0d5857959..6154a0f4455 100644 --- a/src/plugins/eva/utils/export.ml +++ b/src/plugins/eva/utils/export.ml @@ -134,15 +134,14 @@ let frange ~kind (exp : Exp.exp) = function | None -> True | Some(a,b) -> pand (fmin ~kind exp a) (fmax ~kind exp b) -let fval ~kind (exp : Exp.exp) (fval : Fval.t) : pred = +let fval typ (exp : Exp.exp) (fval : Fval.t) : pred = + let kind = + match typ with + | TFloat(kind,_) -> kind + | _ -> assert false in let range,isNaN = Fval.min_and_max fval in por (fNaN exp isNaN) (frange ~kind exp range) -let fkind (typ : typ) = - match typ with - | TFloat(kind,_) -> kind - | _ -> assert false - (* -------------------------------------------------------------------------- *) (* --- Values --- *) (* -------------------------------------------------------------------------- *) @@ -151,14 +150,10 @@ type value = Results.value Results.evaluation let domain (exp : Exp.exp) typ (value : value) : pred = if Cil.isIntegralType typ then - match Results.as_ival value with - | Ok v -> ival exp v - | Error err -> error err + Results.as_ival value |> Result.fold ~error ~ok:(ival exp) else if Cil.isFloatingType typ then - match Results.as_fval value with - | Ok v -> fval ~kind:(fkind typ) exp v - | Error err -> error err + Results.as_fval value |> Result.fold ~error ~ok:(fval typ exp) else True (* -------------------------------------------------------------------------- *) -- GitLab