Skip to content

Commit d240b86

Browse files
Use ID.ge/ID.lt instead of ID.minimal/ID.maximal in check_shift_neg
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/fd400683-08ae-4a0a-b4ff-458d87ba80f8 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent 9292a45 commit d240b86

1 file changed

Lines changed: 5 additions & 3 deletions

File tree

src/analyses/base.ml

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -227,10 +227,12 @@ struct
227227
(* Check the shift amount for negative values (undefined behavior in C), emitting
228228
appropriate warnings/errors based on bounds analysis. *)
229229
let check_shift_neg dir y =
230-
match ID.minimal y, ID.maximal y with
231-
| Some min_y, _ when Z.geq min_y Z.zero ->
230+
let ik = ID.ikind y in
231+
let zero = ID.of_int ik Z.zero in
232+
match ID.ge y zero, ID.lt y zero with
233+
| Some true, _ ->
232234
Checks.safe Checks.Category.InvalidShift
233-
| _, Some max_y when Z.lt max_y Z.zero ->
235+
| _, Some true ->
234236
M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-%s by negative amount is undefined behavior" dir;
235237
Checks.error Checks.Category.InvalidShift "Shift-%s by negative amount is undefined behavior" dir
236238
| _ ->

0 commit comments

Comments
 (0)