Add cram test for YAML violation witness refutation

tests/regression/witness/violation.t/correct-hard.c

@@ -0,0 +1,9 @@
+void reach_error(){}
+extern int __VERIFIER_nondet_int();
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+  if (x != x)
+    reach_error();
+  return 0;
+}

tests/regression/witness/violation.t/correct-hard.yml

@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019e
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct-hard.c
+      input_file_hashes:
+        correct-hard.c: 5cc49c1ce5a9aef64286c2a6e57f6955c5f4f9b19b43056507ae87a802802447
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct-hard.c
+          line: 7
+          column: 5
+          function: main

tests/regression/witness/violation.t/correct.c

@@ -0,0 +1,5 @@
+void reach_error(){}
+
+int main() {
+  return 0;
+}

tests/regression/witness/violation.t/correct.yml

@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019d
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct.c
+      input_file_hashes:
+        correct.c: 6f760cf7f33fc152738bf3514fe623cc94e52cad9ddc2f0e744595ce0de07530
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct.c
+          line: 4
+          column: 3
+          function: main

tests/regression/witness/violation.t/incorrect.c

@@ -0,0 +1,6 @@
+void reach_error(){}
+
+int main() {
+  reach_error();
+  return 0;
+}

tests/regression/witness/violation.t/incorrect.yml

@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019c
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - incorrect.c
+      input_file_hashes:
+        incorrect.c: 1af4fd9e76418e4b95af9950b58248127e7c2d9eb791e1c9b92da53952e0fca2
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: incorrect.c
+          line: 4
+          column: 3
+          function: main

tests/regression/witness/violation.t/run.t

@@ -0,0 +1,57 @@
+Violation witness for a correct program can be refuted by proving the program correct and returning `true`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 1 (1 in uncalled functions)
+    total lines: 3
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: true
+
+If a correct progtam cannot be proven correct, return `unknown` for the violation witness:
+
+  $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown
+
+Violation witness for an incorrect program cannot be proven correct, so return `unknown`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown