Skip to content

Commit 5d9e460

Browse files
Use Behavior.Undefined.other category for shift-by-negative warnings
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c81d432d-7783-4469-9c48-85d6bb3d1531 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent fad313c commit 5d9e460

1 file changed

Lines changed: 4 additions & 4 deletions

File tree

src/analyses/base.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -280,10 +280,10 @@ struct
280280
(match shift_amount_negcheck y with
281281
| `NonNeg -> Checks.safe Checks.Category.InvalidShift
282282
| `Neg ->
283-
M.error ~category:M.Category.Integer.overflow ~tags:[CWE 758] "Shift-left by negative amount is undefined behavior";
283+
M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-left by negative amount is undefined behavior";
284284
Checks.error Checks.Category.InvalidShift "Shift-left by negative amount is undefined behavior"
285285
| `MayNeg ->
286-
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 758] "Shift-left by possibly negative amount may be undefined behavior";
286+
M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-left by possibly negative amount may be undefined behavior";
287287
Checks.warn Checks.Category.InvalidShift "Shift-left by possibly negative amount may be undefined behavior");
288288
ID.shift_left x y
289289
| Shiftrt ->
@@ -292,10 +292,10 @@ struct
292292
(match shift_amount_negcheck y with
293293
| `NonNeg -> Checks.safe Checks.Category.InvalidShift
294294
| `Neg ->
295-
M.error ~category:M.Category.Integer.overflow ~tags:[CWE 758] "Shift-right by negative amount is undefined behavior";
295+
M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-right by negative amount is undefined behavior";
296296
Checks.error Checks.Category.InvalidShift "Shift-right by negative amount is undefined behavior"
297297
| `MayNeg ->
298-
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 758] "Shift-right by possibly negative amount may be undefined behavior";
298+
M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-right by possibly negative amount may be undefined behavior";
299299
Checks.warn Checks.Category.InvalidShift "Shift-right by possibly negative amount may be undefined behavior");
300300
ID.shift_right x y
301301
| LAnd -> id_binary_log (&&) ~annihilator:false result_ik

0 commit comments

Comments
 (0)