diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c index e6f2d5d429..e18c8e0499 100644 --- 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 #include diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c index 2fa3530679..22384b9238 100644 --- 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 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 index 9311af8306..a8fee12c79 100644 --- 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