Add cram test for vojdani privatization flow-insensitive invariants

Author: sim642

tests/regression/13-privatized/74-mutex.t

@@ -277,7 +277,102 @@ Same with ghost_instrumentation and invariant_set entries.
         value: '! multithreaded || (m_locked || used == 0)'
         format: c_expression
 
-Same with mutex-meet.
+Same protected invariant with vojdani but no unprotected invariant.
+
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c
+  [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)
+  [Warning][Deadcode] Function 'producer' has dead code:
+    on line 26 (74-mutex.c:26-26)
+  [Warning][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 1
+    total lines: 15
+  [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11)
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 1
+    total generation entries: 2
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: ghost_instrumentation
+    content:
+      ghost_variables:
+      - name: m_locked
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      - name: multithreaded
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      ghost_updates:
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 20
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 23
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 34
+          column: 3
+          function: main
+        updates:
+        - variable: multithreaded
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 36
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 38
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          value: "0"
+          format: c_expression
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m_locked || used == 0)'
+      type: assertion
+      format: C
+
+Same as protection with mutex-meet.
 
   $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c
   [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)

tests/regression/56-witness/64-ghost-multiple-protecting.t

@@ -337,6 +337,168 @@ protection-read has precise protected invariant for g2.
       type: assertion
       format: C
 
+  $ goblint --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 2
+    total generation entries: 3
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+vojdani has precise protected invariant for g2, but no unprotected invariants.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: ghost_instrumentation
+    content:
+      ghost_variables:
+      - name: m1_locked
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      - name: m2_locked
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      - name: multithreaded
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      ghost_updates:
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 9
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 10
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 14
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 16
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 19
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 20
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 22
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 23
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 29
+          column: 3
+          function: main
+        updates:
+        - variable: multithreaded
+          value: "1"
+          format: c_expression
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m2_locked || (m1_locked || g2 == 0))'
+      type: assertion
+      format: C
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m2_locked || (m1_locked || g1 == 0))'
+      type: assertion
+      format: C
+
   $ goblint --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 19