Merge pull request #1905 from goblint/overflow-kind-minus

Distinguish unary and binary minus in overflow messages

Author: sim642

src/cdomain/value/cdomains/intDomain0.ml

@@ -88,6 +88,9 @@ let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
     let sign = if signed then "Signed" else "Unsigned" in
     let op =
       match op with
+      (* explicitly distinguish binary and unary - *)
+      | Binop (MinusA | MinusPP | MinusPI) -> "binary -" (* only MinusA should probably be possible here *)
+      | Unop Neg -> "unary -"
       | Binop bop -> CilType.Binop.show bop
       | Unop uop -> CilType.Unop.show uop
       | Cast -> "cast"

tests/regression/29-svcomp/32-no-ov.t

@@ -3,7 +3,8 @@
   [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
   [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in << (32-no-ov.c:5:6-5:159)
   [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in << (32-no-ov.c:5:6-5:159)
-  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow in - (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow in unary - (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow in binary - (32-no-ov.c:5:6-5:159)
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in cast (32-no-ov.c:5:6-5:159)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 3

tests/regression/cfg/foo.t/run.t

@@ -61,7 +61,7 @@
 
   $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant", "loop_invariant"]' --set sem.int.signed_overflow assume_none foo.c
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in + (foo.c:4:5-4:8)
-  [Warning][Integer > Overflow][CWE-191] Signed integer underflow in - (foo.c:5:5-5:8)
+  [Warning][Integer > Overflow][CWE-191] Signed integer underflow in binary - (foo.c:5:5-5:8)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6
     dead: 0

tests/regression/cfg/issue-1356.t/run.t

@@ -93,7 +93,7 @@
 
 
   $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' issue-1356.c
-  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in - (issue-1356.c:11:10-11:15)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in binary - (issue-1356.c:11:10-11:15)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 13
     dead: 0