Skip to content

Commit

Permalink
dune promote
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Dec 17, 2024
1 parent ced9396 commit 1795a2b
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions tests/regression/46-apron2/96-witness-mm-escape2.t
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,6 @@
total generation entries: 6

$ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --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
Expand All @@ -20,3 +16,7 @@
unsupported: 1
disabled: 0
total validation entries: 9
[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 != 0 (96-witness-mm-escape2.c:22:1)
[Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)

0 comments on commit 1795a2b

Please sign in to comment.