diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index d5b65a95f4..51a27e19f8 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -785,8 +785,7 @@ struct | TFloat (fk, _), FLongDouble | TFloat (FDouble as fk, _), FDouble | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st - | TInt (ik, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *) - | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) st) + | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st) | CastE ((TInt (ik, _)) as t, e), Int c | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *) (match eval e st with diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c index 46512aed21..b121645b27 100644 --- a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c +++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c @@ -6,7 +6,7 @@ int main() { int64_t data; if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL)) { - int64_t result = data * data; // NOWARN + int64_t result = data * data; // TODO NOWARN } return 8; }