Add manual witness for 56-witness/62-tm-inv-transfer-protection-witness

Author: sim642

tests/regression/56-witness/62-tm-inv-transfer-protection-witness-manual.yml

@@ -0,0 +1,34 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: a3819e93-2ad6-42fd-aee8-f25aac0eb212
+    creation_time: 2025-03-07T15:04:22Z
+    producer:
+      name: Vesal Vojdani
+      version: n/a
+    task:
+      input_files:
+      - 62-tm-inv-transfer-protection-witness.c
+      input_file_hashes:
+        62-tm-inv-transfer-protection-witness.c: 139627d4167e48c2399f0a6359e533d8ac7597e9b4155c58ddcb2b7bfe780088
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 62-tm-inv-transfer-protection-witness.c
+        line: 27
+        column: 3
+        function: main
+      value: 40 <= g && g <= 41
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 62-tm-inv-transfer-protection-witness.c
+        line: 31
+        column: 3
+        function: main
+      value: 40 <= g && g <= 42
+      format: c_expression

tests/regression/56-witness/62-tm-inv-transfer-protection-witness.t

@@ -0,0 +1,27 @@
+Same as regression test, but with manually written witness from Simmo's PhD thesis:
+
+  $ goblint --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness-manual.yml --enable ana.widen.tokens 62-tm-inv-transfer-protection-witness.c
+  [Info][Witness] unassume invariant: 40 <= g && g <= 41 (62-tm-inv-transfer-protection-witness.c:26:3-26:25)
+  [Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
+  [Warning][Assert] Assertion "g <= 41" is unknown. (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
+  [Info][Witness] unassume invariant: 40 <= g && g <= 42 (62-tm-inv-transfer-protection-witness.c:29:3-29:27)
+  [Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
+  [Success][Assert] Assertion "g <= 42" will succeed (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19
+  [Warning][Race] Memory location g (race with conf. 110): (62-tm-inv-transfer-protection-witness.c:5:5-5:11)
+    write with [lock:{B}, thread:[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:10:3-10:9)
+    write with [lock:{B}, thread:[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:11:3-11:9)
+    write with thread:[main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:17:3-17:9)
+    read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
+    read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
+    read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
+    read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
+  [Info][Race] Memory locations race summary:
+    safe: 0
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 1
+