diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t index b61650c6d3..b5f09616a7 100644 --- a/tests/regression/04-mutex/01-simple_rc.t +++ b/tests/regression/04-mutex/01-simple_rc.t @@ -1,9 +1,9 @@ $ goblint --enable warn.deterministic 01-simple_rc.c [Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13) - write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) - read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index b6c43d21bc..33db951684 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -1,15 +1,15 @@ $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -24,15 +24,15 @@ $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index 0ecf051578..e2afc34125 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) - write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) + write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 611a70a7c3..9b6337a032 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) - write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index 7ddbdc4fd7..1a191fa076 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) - write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct T).s.field (safe): - write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t index 7c79572d88..708d676d1a 100644 --- a/tests/regression/04-mutex/84-distribute-fields-1.t +++ b/tests/regression/04-mutex/84-distribute-fields-1.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c [Warning][Race] Memory location s.data (race with conf. 110): (84-distribute-fields-1.c:9:10-9:11) - write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) - write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) + write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location s (safe): (84-distribute-fields-1.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t index 303c10dccd..6bd8abc1cf 100644 --- a/tests/regression/04-mutex/85-distribute-fields-2.t +++ b/tests/regression/04-mutex/85-distribute-fields-2.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c [Warning][Race] Memory location t.s.data (race with conf. 110): (85-distribute-fields-2.c:15:10-15:11) - write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) - write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) + write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location t.s (safe): (85-distribute-fields-2.c:15:10-15:11) - write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index 084148392c..ea57fd2ba5 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c [Warning][Race] Memory location t.s.data (race with conf. 110): (86-distribute-fields-3.c:15:10-15:11) - write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) - write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) + write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location t (safe): (86-distribute-fields-3.c:15:10-15:11) - write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 diff --git a/tests/regression/04-mutex/87-distribute-fields-4.t b/tests/regression/04-mutex/87-distribute-fields-4.t index 5c26e80592..3c8ac025b0 100644 --- a/tests/regression/04-mutex/87-distribute-fields-4.t +++ b/tests/regression/04-mutex/87-distribute-fields-4.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 87-distribute-fields-4.c [Warning][Race] Memory location s (race with conf. 110): (87-distribute-fields-4.c:9:10-9:11) - write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]}, thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) - write with [mhp:{tid=[main]; created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) + write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 diff --git a/tests/regression/04-mutex/88-distribute-fields-5.t b/tests/regression/04-mutex/88-distribute-fields-5.t index 8f0014e34c..1c32b2ac23 100644 --- a/tests/regression/04-mutex/88-distribute-fields-5.t +++ b/tests/regression/04-mutex/88-distribute-fields-5.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 88-distribute-fields-5.c [Warning][Race] Memory location t.s (race with conf. 110): (88-distribute-fields-5.c:15:10-15:11) - write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]}, thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) - write with [mhp:{tid=[main]; created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) + write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 diff --git a/tests/regression/04-mutex/89-distribute-fields-6.t b/tests/regression/04-mutex/89-distribute-fields-6.t index aeb5050395..56996b4e26 100644 --- a/tests/regression/04-mutex/89-distribute-fields-6.t +++ b/tests/regression/04-mutex/89-distribute-fields-6.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 89-distribute-fields-6.c [Warning][Race] Memory location t (race with conf. 110): (89-distribute-fields-6.c:15:10-15:11) - write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]}, thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) - write with [mhp:{tid=[main]; created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) + write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index 587e943b36..b678e490f8 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) [Success][Race] Memory location (struct T).s (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index afb01fdced..79ab8b4bc2 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17) [Warning][Race] Memory location (struct T).s (race with conf. 100): - write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S) (safe): - write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) [Success][Race] Memory location (struct T) (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index 1748b245e2..913ba9bcc5 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) [Success][Race] Memory location (struct U).t (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 50c72aa289..3ec7b12e63 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -1,17 +1,17 @@ $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29) [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11) - read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11) - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 diff --git a/tests/regression/06-symbeq/14-list_entry_rc.t b/tests/regression/06-symbeq/14-list_entry_rc.t index cfdc54c94c..d70ad0c186 100644 --- a/tests/regression/06-symbeq/14-list_entry_rc.t +++ b/tests/regression/06-symbeq/14-list_entry_rc.t @@ -6,10 +6,10 @@ dead: 0 total lines: 23 [Warning][Race] Memory location (alloc@sid:29@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) - write with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - write with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - read with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - read with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#top] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + read with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#top] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#top]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index b63471a45e..3b97fac458 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -6,8 +6,8 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Warning][Race] Memory location (struct s).datum (race with conf. 100): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) - write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + write with thread:[main, t_fun@16-type_rc.c:35:3-35:37#top] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) [Error][Imprecise][Unsound] Function definition missing @@ -18,7 +18,7 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Success][Race] Memory location (struct s).datum (safe): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with thread:[main, t_fun@16-type_rc.c:35:3-35:37#top] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t index 227c66058e..24b9217bac 100644 --- a/tests/regression/06-symbeq/21-mult_accs_rc.t +++ b/tests/regression/06-symbeq/21-mult_accs_rc.t @@ -8,8 +8,8 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9) [Warning][Race] Memory location (struct s).data (race with conf. 100): - write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) - write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26) [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14) @@ -25,7 +25,7 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9) [Success][Race] Memory location (struct s).data (safe): - write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#top] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26) [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)