Skip to content

Commit 46aeaa1

Browse files
Push
1 parent a841507 commit 46aeaa1

28 files changed

Lines changed: 224 additions & 212 deletions

src/analyses/threadFlag.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ struct
6363
let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in
6464
((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2
6565

66-
(* kill access when single threaded *)
66+
(* kill access when single threaded *)
6767

6868
let should_print m = true
6969
end
Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
$ goblint --enable warn.deterministic 01-simple_rc.c 2>&1 | tee default-output.txt
22
[Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13)
3-
write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
4-
write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
5-
read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
6-
read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
3+
write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
4+
write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
5+
read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
6+
read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
77
[Info][Race] Memory locations race summary:
88
safe: 0
99
vulnerable: 0
@@ -18,13 +18,13 @@
1818

1919
$ diff default-output.txt full-output.txt
2020
2,5c2,5
21-
< write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
22-
< write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
23-
< read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
24-
< read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
21+
< write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
22+
< write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
23+
< read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
24+
< read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
2525
---
26-
> write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
27-
> write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
28-
> read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
29-
> read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
26+
> write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
27+
> write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
28+
> read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
29+
> read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
3030
[1]
Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
$ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-1.txt
22
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
33
[Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
4-
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
5-
read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
4+
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
5+
read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
66
[Info][Race] Memory locations race summary:
77
safe: 1
88
vulnerable: 0
99
unsafe: 1
1010
total memory locations: 2
1111
[Success][Race] Memory location (struct S).field (safe):
12-
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
12+
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
1313
[Info][Deadcode] Logical lines of code (LLoC) summary:
1414
live: 7
1515
dead: 0
@@ -24,15 +24,15 @@
2424
$ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-2.txt
2525
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
2626
[Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
27-
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
28-
read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
27+
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
28+
read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
2929
[Info][Race] Memory locations race summary:
3030
safe: 1
3131
vulnerable: 0
3232
unsafe: 1
3333
total memory locations: 2
3434
[Success][Race] Memory location (struct S).field (safe):
35-
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
35+
write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
3636
[Info][Deadcode] Logical lines of code (LLoC) summary:
3737
live: 7
3838
dead: 0
@@ -48,28 +48,28 @@
4848
4949
$ diff default-output-1.txt full-output-1.txt
5050
3,4c3,4
51-
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
52-
< read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
51+
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
52+
< read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
5353
---
54-
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
55-
> read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
54+
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
55+
> read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
5656
11c11
57-
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
57+
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
5858
---
59-
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
59+
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
6060
[1]
6161
6262
$ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs --enable dbg.full-output 49-type-invariants.c > full-output-2.txt 2>&1
6363
6464
$ diff default-output-2.txt full-output-2.txt
6565
3,4c3,4
66-
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
67-
< read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
66+
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
67+
< read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
6868
---
69-
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
70-
> read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
69+
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
70+
> read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
7171
11c11
72-
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
72+
< write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
7373
---
74-
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
74+
> write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
7575
[1]

tests/regression/04-mutex/77-type-nested-fields.t

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@
22
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20)
33
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22)
44
[Warning][Race] Memory location (struct T).s.field (race with conf. 100):
5-
write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
6-
write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
5+
write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
6+
write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
77
[Info][Race] Memory locations race summary:
88
safe: 1
99
vulnerable: 0
1010
unsafe: 1
1111
total memory locations: 2
1212
[Success][Race] Memory location (struct S).field (safe):
13-
write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
13+
write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
1414
[Info][Deadcode] Logical lines of code (LLoC) summary:
1515
live: 7
1616
dead: 0
@@ -29,13 +29,13 @@
2929

3030
$ diff default-output.txt full-output.txt
3131
4,5c4,5
32-
< write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
33-
< write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
32+
< write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
33+
< write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
3434
---
35-
> write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
36-
> write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
35+
> write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
36+
> write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
3737
12c12
38-
< write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
38+
< write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
3939
---
40-
> write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
40+
> write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
4141
[1]

0 commit comments

Comments
 (0)