Add cram witness test to 56-witness/05-prec-problem

goblint · Feb 8, 2024 · 6c9d719 · 6c9d719
1 parent 11c16bc
commit 6c9d719
Show file tree

Hide file tree

Showing 3 changed files with 97 additions and 2 deletions.
diff --git a/tests/regression/56-witness/05-prec-problem.c b/tests/regression/56-witness/05-prec-problem.c
@@ -1,4 +1,4 @@
-//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types[+] precondition_loop_invariant
+//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]'
 #include <stdlib.h>
 #include <goblint.h>
 
@@ -9,7 +9,7 @@ int foo(int* ptr1, int* ptr2){
     } else {
         result = 1;
     }
-    // Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s]
+    // cram test checks for precondition invariant soundness
     return result;
 }
 

diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t
@@ -0,0 +1,89 @@
+  $ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c
+  [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:21:5-21:28)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 12
+    dead: 0
+    total lines: 12
+  [Info][Witness] witness generation summary:
+    total generation entries: 10
+
+Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`,
+and separately invariants `result == 0` and `result == 1`.
+The sound invariant is `result == 1 || result == 0`.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: result == 1 || result == 0
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: '*ptr2 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: '*ptr1 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 7
+      function: foo
+    loop_invariant:
+      string: '*ptr2 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 7
+      function: foo
+    loop_invariant:
+      string: '*ptr1 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
@@ -0,0 +1,6 @@
+(env
+ (_
+  (binaries ../../util/yamlWitnessStrip.exe)))
+
+(cram
+ (deps (glob_files *.c) %{bin:yamlWitnessStrip}))