From 1730aa71eaa6ba4dfcf6492f3bdf79eeb677f54b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 14:03:50 +0200 Subject: [PATCH] Remove BaseInvariant tmpSpecial TODOs --- src/analyses/baseInvariant.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 0d79aa8969..304d3e55ad 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -714,16 +714,17 @@ struct let tmpSpecial = ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty tmpSpecial; begin match tmpSpecial with - | `Lifted (Abs (_ik, xInt)) -> - inv_exp (Int (ID.join c (ID.neg c))) xInt st (* TODO: deduplicate *) + | `Lifted (Abs (ik, xInt)) -> + let c' = ID.cast_to ik c in (* different ik! *) + inv_exp (Int (ID.join c' (ID.neg c'))) xInt st | tmpSpecial -> - let tv_opt = ID.to_bool c in (* TODO: simplify *) - begin match tv_opt with + begin match ID.to_bool c with | Some tv -> begin match tmpSpecial with | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st (* should be correct according to C99 standard*) + (* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *) | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st