Skip to content

Commit 0450f40

Browse files
committed
Add cram test for issue #1712
1 parent e27c85d commit 0450f40

File tree

1 file changed

+18
-0
lines changed

1 file changed

+18
-0
lines changed

tests/regression/46-apron2/98-issue-1511b.t

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,3 +41,21 @@
4141
[Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:27:5)
4242
[Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:27:5)
4343
[Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5)
44+
45+
46+
# Issue #1712
47+
TODO: Mutex f should read-write protect j as well.
48+
49+
$ goblint --enable warn.deterministic --enable dbg.print_protection --disable ana.dead-code.lines 98-issue-1511b.c
50+
[Info][Race] Mutex f read-write protects 1 variable(s): {nothing2}
51+
[Info][Race] Variable j read-write protected by 1 mutex(es): {f}
52+
[Info][Race] Variable nothing2 read-write protected by 1 mutex(es): {f}
53+
[Info][Race] Memory locations race summary:
54+
safe: 1
55+
vulnerable: 0
56+
unsafe: 0
57+
total memory locations: 1
58+
[Info][Race] Mutex read-write protection summary:
59+
Number of mutexes: 1
60+
Max number variables of protected by a mutex: 1
61+
Total number of protected variables (including duplicates): 1

0 commit comments

Comments
 (0)