File tree Expand file tree Collapse file tree 2 files changed +23
-23
lines changed
tests/regression/13-privatized Expand file tree Collapse file tree 2 files changed +23
-23
lines changed Original file line number Diff line number Diff line change 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 )
1
+ $ goblint -- enable dbg. print_protection -- enable warn . deterministic 19 -publish-precision. c
4
2
[Warning][Assert] Assertion " glob1 == 0" is unknown. (19 -publish-precision. c: 30 : 3 -30: 30 )
5
3
[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
4
+ [Success][Assert] Assertion " glob1 == 5" will succeed (19 -publish-precision. c: 17 : 3 -17: 30 )
5
+ [Success][Assert] Assertion " glob1 == 0" will succeed (19 -publish-precision. c: 27 : 3 -27: 30 )
10
6
[Info][Race] Mutex mutex1 read-write protects 0 variable(s): {}
11
- [Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex2}
12
7
[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
8
+ [Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex2}
17
9
[Info][Race] Memory locations race summary:
18
10
safe: 1
19
11
vulnerable: 0
20
12
unsafe: 0
21
13
total memory locations: 1
14
+ [Info][Race] Mutex read-write protection summary:
15
+ Number of mutexes: 2
16
+ Max number variables of protected by a mutex: 1
17
+ Total number of protected variables (including duplicates): 1
18
+ [Info][Deadcode] Logical lines of code (LLoC) summary:
19
+ live: 20
20
+ dead: 0
21
+ total lines : 20
Original file line number Diff line number Diff line change 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 )
1
+ $ goblint -- enable dbg. print_protection -- enable warn . deterministic 20 -publish-regression. c
3
2
[Success][Assert] Assertion " glob1 == 5" will succeed (20 -publish-regression. c: 20 : 3 -20: 30 )
3
+ [Success][Assert] Assertion " glob1 == 0" will succeed (20 -publish-regression. c: 29 : 3 -29: 30 )
4
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
5
[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
6
[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
7
+ [Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex1}
16
8
[Info][Race] Memory locations race summary:
17
9
safe: 1
18
10
vulnerable: 0
19
11
unsafe: 0
20
12
total memory locations: 1
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][Deadcode] Logical lines of code (LLoC) summary:
18
+ live: 19
19
+ dead: 0
20
+ total lines : 19
You can’t perform that action at this time.
0 commit comments