Skip to content

Commit 4aa0ad2

Browse files
committed
Add protection cram tests for 13-privatized/19-publish-precision and 20-publish-regression
1 parent 0450f40 commit 4aa0ad2

File tree

2 files changed

+41
-0
lines changed

2 files changed

+41
-0
lines changed
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
$ goblint --enable dbg.print_protection 19-publish-precision.c
2+
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
3+
[Success][Assert] Assertion "glob1 == 5" will succeed (19-publish-precision.c:17:3-17:30)
4+
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
5+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
6+
[Info][Deadcode] Logical lines of code (LLoC) summary:
7+
live: 20
8+
dead: 0
9+
total lines: 20
10+
[Info][Race] Mutex mutex1 read-write protects 0 variable(s): {}
11+
[Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex2}
12+
[Info][Race] Mutex mutex2 read-write protects 1 variable(s): {glob1}
13+
[Info][Race] Mutex read-write protection summary:
14+
Number of mutexes: 2
15+
Max number variables of protected by a mutex: 1
16+
Total number of protected variables (including duplicates): 1
17+
[Info][Race] Memory locations race summary:
18+
safe: 1
19+
vulnerable: 0
20+
unsafe: 0
21+
total memory locations: 1
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
$ goblint --enable dbg.print_protection 20-publish-regression.c
2+
[Success][Assert] Assertion "glob1 == 0" will succeed (20-publish-regression.c:29:3-29:30)
3+
[Success][Assert] Assertion "glob1 == 5" will succeed (20-publish-regression.c:20:3-20:30)
4+
[Success][Assert] Assertion "glob1 == 0" will succeed (20-publish-regression.c:32:3-32:30)
5+
[Info][Deadcode] Logical lines of code (LLoC) summary:
6+
live: 19
7+
dead: 0
8+
total lines: 19
9+
[Info][Race] Mutex mutex1 read-write protects 1 variable(s): {glob1}
10+
[Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex1}
11+
[Info][Race] Mutex mutex2 read-write protects 0 variable(s): {}
12+
[Info][Race] Mutex read-write protection summary:
13+
Number of mutexes: 2
14+
Max number variables of protected by a mutex: 1
15+
Total number of protected variables (including duplicates): 1
16+
[Info][Race] Memory locations race summary:
17+
safe: 1
18+
vulnerable: 0
19+
unsafe: 0
20+
total memory locations: 1

0 commit comments

Comments
 (0)