Skip to content

Commit

Permalink
fix overflow analysis
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Feb 1, 2024
1 parent f483830 commit 3a0318a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1286,7 +1286,7 @@ struct
(* check if the current operation causes a signed overflow *)
begin match unop with
| Neg -> (* an overflow happens when the lower bound of the interval is less than MIN_INT *)
Cil.isSigned ik && checkPredicate e (Z.geq)
Cil.isSigned ik && checkPredicate e (Z.gt)
(* operations that do not result in overflow in C: *)
| BNot|LNot -> false
end
Expand Down

0 comments on commit 3a0318a

Please sign in to comment.