Skip to content

Commit

Permalink
Revert "Add hacky imaxabs sqrt refine support"
Browse files Browse the repository at this point in the history
This reverts commit f9765da.
  • Loading branch information
sim642 committed Oct 16, 2024
1 parent 85cbda6 commit 2f5b50f
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 3 deletions.
3 changes: 1 addition & 2 deletions src/analyses/baseInvariant.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

0 comments on commit 2f5b50f

Please sign in to comment.