Add test for synthetic YAML witness invariant locations (PR #758)

Author: sim642

tests/regression/pr-758.t/pr-758.c

@@ -0,0 +1,22 @@
+// Code from https://github.com/goblint/cil/pull/98
+
+int main() {
+  // for loop
+  int x = 42;
+  for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line
+    // ...
+  }
+
+  // expression with side effect
+  int i, k;
+  i = k = 0; // there shouldn't be invariant k == 0 before this line
+
+  // compound initializers
+  struct kala {
+    int kaal;
+    int hind;
+  };
+
+  struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line
+  return 0;
+}

tests/regression/pr-758.t/run.t

@@ -0,0 +1,31 @@
+  $ goblint --enable ana.int.interval --enable witness.yaml.enabled pr-758.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total: 6
+  [Info][Witness] witness generation summary:
+    total: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: loop_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $STRIPPED_FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    loop_invariant:
+      string: a.hind == 3
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $STRIPPED_FILE_HASH
+      line: 20
+      column: 14
+      function: main
+    loop_invariant:
+      string: i == 0
+      type: assertion
+      format: C