Fix GobApron.Linxexpr0.neg not negating all dimensions

Author: sim642

src/cdomains/apron/gobApron.apron.ml

@@ -44,11 +44,10 @@ struct
   (** Negate linear expression. *)
   let neg (linexpr0: t): t =
     let r = copy linexpr0 in
-    let n = Linexpr0.get_size r in
-    for i = 0 to n - 1 do
-      Linexpr0.set_coeff r i (Coeff.neg (Linexpr0.get_coeff r i))
-    done;
-    Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst r));
+    Linexpr0.iter (fun c i ->
+        Linexpr0.set_coeff r i (Coeff.neg c)
+      ) linexpr0;
+    Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst linexpr0));
     r
 end
 

tests/regression/36-apron/01-octagon_simple.t

@@ -21,7 +21,7 @@ Without diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (01-octagon_simple.c:44:10-44:11)
   [Info][Witness] witness generation summary:
     location invariants: 0
-    loop invariants: 14
+    loop invariants: 16
     flow-insensitive invariants: 0
     total generation entries: 1
 
@@ -64,6 +64,15 @@ Without diff-box:
           function: main
         value: (long long )X + 2147483647LL >= (long long )N
         format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 01-octagon_simple.c
+          line: 10
+          column: 3
+          function: main
+        value: (long long )X >= 0LL
+        format: c_expression
     - invariant:
         type: loop_invariant
         location:
@@ -127,6 +136,15 @@ Without diff-box:
           function: two
         value: (long long )X + 2147483647LL >= (long long )N
         format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 01-octagon_simple.c
+          line: 44
+          column: 3
+          function: two
+        value: (long long )X >= 0LL
+        format: c_expression
     - invariant:
         type: loop_invariant
         location:
@@ -253,6 +271,15 @@ Compare witnesses:
         function: two
       value: 2147483647LL >= (long long )N
       format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 44
+        column: 3
+        function: two
+      value: (long long )X >= 0LL
+      format: c_expression
   - invariant:
       type: loop_invariant
       location:
@@ -289,6 +316,15 @@ Compare witnesses:
         function: main
       value: 2147483647LL >= (long long )N
       format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 10
+        column: 3
+        function: main
+      value: (long long )X >= 0LL
+      format: c_expression
   - invariant:
       type: loop_invariant
       location:

tests/regression/89-apron3/03-octagon_simplest.t

@@ -8,11 +8,10 @@ Without diff-box:
   [Warning][Deadcode][CWE-570] condition 'N < 0' is always false (03-octagon_simplest.c:9:6-9:11)
   [Info][Witness] witness generation summary:
     location invariants: 0
-    loop invariants: 15
+    loop invariants: 17
     flow-insensitive invariants: 0
     total generation entries: 1
 
-TODO: Should have Y == 0
   $ yamlWitnessStrip < witness.yml | tee witness-disable-diff-box.yml
   - entry_type: invariant_set
     content:
@@ -70,6 +69,15 @@ TODO: Should have Y == 0
           function: main
         value: (long long )X >= (long long )Y
         format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 03-octagon_simplest.c
+          line: 11
+          column: 3
+          function: main
+        value: (long long )X >= 0LL
+        format: c_expression
     - invariant:
         type: loop_invariant
         location:
@@ -106,6 +114,15 @@ TODO: Should have Y == 0
           function: main
         value: (long long )Y + 2147483647LL >= (long long )X
         format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 03-octagon_simplest.c
+          line: 11
+          column: 3
+          function: main
+        value: (long long )Y == 0LL
+        format: c_expression
     - invariant:
         type: loop_invariant
         location:
@@ -238,6 +255,15 @@ Compare witnesses:
         function: main
       value: 2147483647LL >= (long long )N
       format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 03-octagon_simplest.c
+        line: 11
+        column: 3
+        function: main
+      value: (long long )Y == 0LL
+      format: c_expression
   - invariant:
       type: loop_invariant
       location:
@@ -265,6 +291,15 @@ Compare witnesses:
         function: main
       value: (long long )Y + (long long )N >= 0LL
       format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 03-octagon_simplest.c
+        line: 11
+        column: 3
+        function: main
+      value: (long long )X >= 0LL
+      format: c_expression
   - invariant:
       type: loop_invariant
       location: