affeq: Fix array OOB in invariant

Author: michael-schwarz

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -681,7 +681,7 @@ struct
   let invariant t =
     let invariant m =
       let earray = Lincons1.array_make t.env (Matrix.num_rows m) in
-      for i = 0 to Lincons1.array_length earray do
+      for i = 0 to (Lincons1.array_length earray -1) do
         let row = Matrix.get_row m i in
         let coeff_vars = List.map (fun x ->  Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in
         let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in

tests/regression/63-affeq/19-witness.c

@@ -0,0 +1,18 @@
+//SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none --set ana.relation.privatization top --enable witness.yaml.enabled
+// Identical to Example 63/01; additionally checking that writing out witnesses does not crash the analyzer
+#include <goblint.h>
+
+void main(void) {
+    int i;
+    int j;
+    int k;
+    i = 2;
+    j = k + 5;
+
+    while (i < 100) {
+        __goblint_check(3 * i - j + k == 1);
+        i = i + 1;
+        j = j + 3;
+    }
+    __goblint_check(3 * i - j + k == 1);
+}