Add test for incorrect YAML witness invariant locations from CIL tran…

…sformations (issue #1356)

tests/regression/issue-1356.t/issue-1356.c

@@ -0,0 +1,20 @@
+extern int  __VERIFIER_nondet_int(void);
+
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+
+int minus(int a, int b) {
+  assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line
+  assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line
+  return a - b;
+}
+
+int main() {
+  int x, y;
+  x = __VERIFIER_nondet_int();
+  y = __VERIFIER_nondet_int();
+  minus(x, y);
+  return 0;
+}

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

@@ -0,0 +1,12 @@
+  $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:3-11:15)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 13
+    dead: 0
+    total lines: 13
+  [Info][Witness] witness generation summary:
+    total generation entries: 4
+
+  $ yamlWitnessStrip < witness.yml
+  []