-
Notifications
You must be signed in to change notification settings - Fork 75
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Co-authored-by: Simmo Saan <[email protected]>
- Loading branch information
1 parent
916acfa
commit d6c5bba
Showing
7 changed files
with
136 additions
and
136 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,29 +1,29 @@ | ||
| $ goblint --enable allglobs 77-type-nested-fields.c | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) | ||
| $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Warning][Race] Memory location (struct T).s.field (race with conf. 100): | ||
| write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) | ||
| write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:39:3-39:22) | ||
| [Success][Race] Memory location (struct S).field (safe): | ||
| write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, [email protected]:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) | ||
| [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:38:3-38:40#top]}, thread:[main, [email protected]:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,24 +1,6 @@ | ||
| $ goblint --enable allglobs 79-type-nested-fields-deep1.c | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Success][Race] Memory location (struct S).field (safe): | ||
| write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, [email protected]:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [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:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) | ||
|
|
@@ -27,3 +9,21 @@ | |
| 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:43:3-43:40#top]}, thread:[main, [email protected]:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,24 +1,6 @@ | ||
| $ goblint --enable allglobs 80-type-nested-fields-deep2.c | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Success][Race] Memory location (struct T).s.field (safe): | ||
| write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, [email protected]:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [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:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| write with [mhp:{tid=[main]; created={[main, [email protected]:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:44:3-44:24) | ||
|
|
@@ -27,3 +9,21 @@ | |
| 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:43:3-43:40#top]}, thread:[main, [email protected]:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) | ||
| [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,31 +1,31 @@ | ||
| $ goblint --enable allglobs 90-distribute-fields-type-1.c | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) | ||
| $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Success][Race] Memory location (struct T).s (safe): | ||
| write with [mhp:{tid=[main]; created={[main, [email protected]:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40: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:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) | ||
| write with [mhp:{tid=[main]; created={[main, [email protected]:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Success][Race] Memory location (struct S).field (safe): | ||
| write with [mhp:{tid=[main, [email protected]:38:3-38:40#top]}, thread:[main, [email protected]:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [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, [email protected]:38:3-38:40#top]}, thread:[main, [email protected]:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Success][Race] Memory location (struct T).s (safe): | ||
| write with [mhp:{tid=[main]; created={[main, [email protected]:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Deadcode] Logical lines of code (LLoC) summary: | ||
| live: 7 | ||
| dead: 0 | ||
| total lines: 7 | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) | ||
| [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) | ||
| [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) |
Oops, something went wrong.