Merge pull request #1327 from goblint/affeq_witnesses

`affeq`: Fix array OOB in `invariant`

Author: michael-schwarz

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -680,19 +680,15 @@ 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
+      let one_constraint i =
         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
-        Lincons1.set_list (Lincons1.array_get earray i) coeff_vars (Some cst)
-      done;
-      let {lincons0_array; array_env}: Lincons1.earray = earray in
-      Array.enum lincons0_array
-      |> Enum.map (fun (lincons0: Lincons0.t) ->
-          Lincons1.{lincons0; env = array_env}
-        )
-      |> List.of_enum
+        let e1 = Linexpr1.make t.env in
+        Linexpr1.set_list e1 coeff_vars (Some cst);
+        Lincons1.make e1 EQ
+      in
+      List.init (Matrix.num_rows m) one_constraint
     in
     BatOption.map_default invariant [] t.d
 

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

@@ -0,0 +1,34 @@
+//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);
+
+    // Represented with fractional coefficients and thus not put into witness yet
+
+    int a = 0;
+    int b = 0;
+    int z = 0;
+
+    while(z < 100) {
+        a++;
+        b += 2;
+        z++;
+
+        __goblint_check(2*z - b == 0);
+        // b == 2*z is put into the witness
+    }
+
+}