Skip to content

Commit 68acaef

Browse files
authored
Merge pull request #1910 from goblint/abs-speculating
Fix spurious unary - overflow check in `abs` implementation
2 parents db15e2e + 9384f28 commit 68acaef

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/analyses/base.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2665,7 +2665,8 @@ struct
26652665
| _, None
26662666
| None, _ -> ID.top_of ik
26672667
| Some mx, Some mm when Z.equal mx mm -> ID.top_of ik
2668-
| _, _ ->
2668+
| _, _ -> (* ID.neg will not overflow *)
2669+
let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in (* ID.neg is our internal implementation of abs *)
26692670
let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
26702671
let x2 = ID.meet (ID.starting ik Z.zero) xcast in
26712672
ID.join x1 x2

0 commit comments

Comments
 (0)