Add vojdani privatization to 13-privatized/01-priv_nr cram test

goblint · Dec 30, 2024 · c6a2c9e · c6a2c9e
1 parent 040772c
commit c6a2c9e
Showing 1 changed file with 57 additions and 0 deletions.
diff --git a/tests/regression/13-privatized/01-priv_nr.t b/tests/regression/13-privatized/01-priv_nr.t
@@ -55,6 +55,63 @@
       type: assertion
       format: C
 
+`vojdani` privatization:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization vojdani 01-priv_nr.c
+  [Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
+  [Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
+  [Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
+  [Success][Assert] Assertion "glob1 == 6" will succeed (01-priv_nr.c:26:3-26:30)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19
+  [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 3
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 01-priv_nr.c
+      file_hash: $FILE_HASH
+      line: 25
+      column: 3
+      function: main
+    location_invariant:
+      string: glob1 == 5
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 01-priv_nr.c
+      file_hash: $FILE_HASH
+      line: 11
+      column: 3
+      function: t_fun
+    location_invariant:
+      string: glob1 == 5
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 01-priv_nr.c
+      file_hash: $FILE_HASH
+      line: 11
+      column: 3
+      function: t_fun
+    location_invariant:
+      string: (unsigned long )arg == 0UL
+      type: assertion
+      format: C
+
 `mutex-meet` privatization:
 
   $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization mutex-meet 01-priv_nr.c