Update tests

goblint · Dec 17, 2024 · 267f25e · 267f25e
1 parent 775c15f
commit 267f25e
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 5 deletions.
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
 #include <pthread.h>
 #include <goblint.h>
 

diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
 #include<pthread.h>
 int *b;
 pthread_mutex_t e;

diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -1,18 +1,22 @@
   $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
   [Info][Witness] witness generation summary:
-    total generation entries: 5
+    location invariants: 8
+    loop invariants: 0
+    flow-insensitive invariants: 1
+    total generation entries: 6
 
   $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
   [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
   [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Warning][Witness] cannot validate entry of type flow_insensitive_invariant
   [Info][Witness] witness validation summary:
     confirmed: 8
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
-    unsupported: 0
+    unsupported: 1
     disabled: 0
-    total validation entries: 8
+    total validation entries: 9