Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Small output readability improvements #1312

Merged
merged 37 commits into from
Feb 26, 2024
Merged

Small output readability improvements #1312

Show file tree
Hide file tree
Changes from 23 commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
55f51df
Add test for not repeating constants in intervals in warning outputs
karoliineh Dec 28, 2023
4d31efa
Move functions same and to_int upwards
karoliineh Dec 28, 2023
3713f67
Do not repeat constants in intervals in warning outputs
karoliineh Dec 28, 2023
74a333a
Fix missing parentheses in cram test
karoliineh Dec 28, 2023
b41967d
Add --disable warn.info hack for MacOS CI build
karoliineh Dec 28, 2023
adafde1
Remove initial cram test
karoliineh Jan 2, 2024
45d818b
Modify regtest 01 74 to include unknown case
karoliineh Jan 2, 2024
151bf5f
Add cram test for 01-oob-heap-simple
karoliineh Jan 2, 2024
68f5fba
Prettify top intervals (Unknown int([-63,63]),[-9223372036854775808,9…
karoliineh Jan 2, 2024
5b00197
Add cram test for not printing malloc uniqueness counter when disabled
karoliineh Jan 2, 2024
47e11ee
Do not print disabled malloc uniqueness counter
karoliineh Jan 2, 2024
53f8cc2
Add cram test for 87-casts-dep-on-param.c
karoliineh Jan 2, 2024
5e10539
Do not print top thread ID in warnings
karoliineh Jan 2, 2024
df5a698
Add cram test for 14-list_entry_rc.c
karoliineh Jan 2, 2024
19fe5fc
Do not print def_exc domain name in case of constant
karoliineh Jan 2, 2024
1864fed
Make IntDomLifter show similar to pretty
karoliineh Jan 2, 2024
4a90a97
Promote cram test 14-list_entry_rc
karoliineh Jan 2, 2024
cf8d588
Modify cram tests to not repeat tid in mhp in warnings
karoliineh Jan 3, 2024
8ffcc4f
Remove duplicated tid printing from mhp
karoliineh Jan 3, 2024
d0a2a28
Do not print mhp results when empty
karoliineh Jan 3, 2024
2d91b7a
Remove excessive top thread id uniqueness counter from cram tests
karoliineh Jan 3, 2024
2686841
Do not show excessive top thread id uniqueness counter in warnings
karoliineh Jan 3, 2024
51dfd45
Make printXml functions consistent with show and pretty
karoliineh Jan 10, 2024
2cc5e7d
Replace sid-s in cram tests for macos tests to pass
karoliineh Feb 13, 2024
5a397bc
Add dbg.full-output option for getting 'old' output
karoliineh Feb 13, 2024
6f83a80
Add cram tests with dbg.full-output for testing mhp, thread ID and ma…
karoliineh Feb 13, 2024
313d821
Use dbg.full-output option in mHP, threadId and wrapperFunction
karoliineh Feb 13, 2024
4cfd2bc
Add cram tests with dbg.full-output for testing intervals
karoliineh Feb 13, 2024
1148df3
Use dbg.full-output option in intDomain
karoliineh Feb 13, 2024
cc689ce
Indentation
karoliineh Feb 13, 2024
a9d5358
Simplify show in threadIdDomain
karoliineh Feb 14, 2024
0ad7f6f
Merge branch 'master' into issue-1192
karoliineh Feb 14, 2024
5419d44
Use diffs in cram tests
karoliineh Feb 14, 2024
c28e863
Use dbg.full-output in printXml
karoliineh Feb 14, 2024
cfd6b0e
tID #top -> ⊤ and change cram tests accordingly
karoliineh Feb 14, 2024
24b6664
Update dbg.full-output description in options.schema.json
karoliineh Feb 14, 2024
f4d5a45
Merge branch 'master' into issue-1192
karoliineh Feb 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion src/analyses/mHPAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ struct
include MHP
let name () = "mhp"
let may_race = MHP.may_happen_in_parallel
let should_print _ = true
let should_print {tid; created; must_joined} =
not (ConcDomain.ThreadSet.is_empty created)
|| not (ConcDomain.ThreadSet.is_empty must_joined)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How is this an improvement? All this information is needed to understand why accesses are considered racy.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In mhp.ml these exact conditions are already used to not show empty sets. This just means we don't print mhp:{} without anything in it.

We also don't print empty locksets etc. Everything we analyze and print for accesses is what we have for why access are not racy, i.e. information that can rule something out. If we don't have any excluding information (e.g. no locks), then we don't print that we don't know it. If we printed everything we didn't know, we'd have to print complete states.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, for must-joined I guess this holds.
An empty created set is very strong information though (no information would be top).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the created set is empty, we're already single-threaded and that's already reflected by the thread flag.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the created set is empty, we're already single-threaded and that's already reflected by the thread flag.

I'm not sure that's true: The created set is relative to the things the current thread created: We may be in a multi-threaded setting and I may not be the main thread but unique. Then an empty created set means that none of my children can be created yet.

end

let access ctx _: MHP.t = MHP.current (Analyses.ask_of_ctx ctx)
Expand Down
15 changes: 13 additions & 2 deletions src/analyses/wrapperFunctionAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,8 +131,19 @@ module MallocWrapper : MCPSpec = struct
CilType.Location.show loc

let name_varinfo (t, node, c) =
Format.asprintf "(alloc@sid:%s@tid:%s(#%s))" (Node.show_id node) (ThreadLifted.show t) (UniqueCount.show c)

let uniq_count =
if UniqueCount.is_top c then
Format.dprintf ""
sim642 marked this conversation as resolved.
Show resolved Hide resolved
else
Format.dprintf "(#%s)" (UniqueCount.show c)
in
let tid =
if ThreadLifted.is_top t then
sim642 marked this conversation as resolved.
Show resolved Hide resolved
Format.dprintf ""
else
Format.dprintf "@tid:%s%t" (ThreadLifted.show t) uniq_count
in
Format.asprintf "(alloc@sid:%s%t)" (Node.show_id node) tid
sim642 marked this conversation as resolved.
Show resolved Hide resolved
end

module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)
Expand Down
59 changes: 45 additions & 14 deletions src/cdomains/intDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -407,10 +407,22 @@ struct
let widen = lift2 I.widen
let narrow = lift2 I.narrow

let show x = I.show x.v (* TODO add ikind to output *)
let pretty () x = I.pretty () x.v (* TODO add ikind to output *)
let show x =
if I.is_top_of x.ikind x.v then
"⊤"
else
I.show x.v (* TODO add ikind to output *)
let pretty () x =
if I.is_top_of x.ikind x.v then
Pretty.text "⊤"
else
I.pretty () x.v (* TODO add ikind to output *)
let pretty_diff () (x, y) = I.pretty_diff () (x.v, y.v) (* TODO check ikinds, add them to output *)
let printXml o x = I.printXml o x.v (* TODO add ikind to output *)
let printXml o x =
if I.is_top_of x.ikind x.v then
BatPrintf.fprintf o "<value>\n<data>\n⊤\n</data>\n</value>\n"
else
I.printXml o x.v (* TODO add ikind to output *)
(* This is for debugging *)
let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
let to_yojson x = I.to_yojson x.v
Expand Down Expand Up @@ -3590,9 +3602,27 @@ module IntDomTupleImpl = struct
in
mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_incl_list } x |> flat merge

let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in
if n = 1 then Some (List.hd xs)
else (
if n>1 then Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
None
)
let to_int = same BI.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }

let pretty () = (fun xs -> text "(" ++ (try List.reduce (fun a b -> a ++ text "," ++ b) xs with Invalid_argument _ -> nil) ++ text ")") % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> (* assert sf==I.short; *) I.pretty () } (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)

let pretty () x =
match to_int x with
| Some v -> Pretty.text (BI.to_string v)
| None ->
mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> (* assert sf==I.short; *) I.pretty () } x
|> to_list
|> (fun xs ->
text "(" ++ (
try
List.reduce (fun a b -> a ++ text "," ++ b) xs
with Invalid_argument _ ->
nil)
++ text ")") (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)

let refine_functions ik : (t -> t) list =
let maybe reffun ik domtup dom =
Expand Down Expand Up @@ -3688,18 +3718,16 @@ module IntDomTupleImpl = struct
if List.mem `Eq xs then `Eq else
if List.mem `Neq xs then `Neq else
`Top
let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in
if n = 1 then Some (List.hd xs)
else (
if n>1 then Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
None
)
let to_int = same BI.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
let to_bool = same string_of_bool % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.to_bool }
let minimal = flat (List.max ~cmp:BI.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }
let maximal = flat (List.min ~cmp:BI.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.maximal }
(* others *)
let show = String.concat "; " % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) }
let show x =
match to_int x with
karoliineh marked this conversation as resolved.
Show resolved Hide resolved
| Some v -> BI.to_string v
| None -> mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) } x
|> to_list
|> String.concat "; "
let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
let hash = List.fold_left (lxor) 0 % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.hash }

Expand Down Expand Up @@ -3809,7 +3837,10 @@ module IntDomTupleImpl = struct

(* printing boilerplate *)
let pretty_diff () (x,y) = dprintf "%a instead of %a" pretty x pretty y
let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
let printXml f x =
match to_int x with
| Some v -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (BI.to_string v)
karoliineh marked this conversation as resolved.
Show resolved Hide resolved
| None -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)

let invariant_ikind e ik x =
match to_int x with
Expand Down
3 changes: 1 addition & 2 deletions src/cdomains/mHP.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ let current (ask:Queries.ask) =
}

let pretty () {tid; created; must_joined} =
let tid_doc = Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) in
michael-schwarz marked this conversation as resolved.
Show resolved Hide resolved
(* avoid useless empty sets in race output *)
let created_doc =
if ConcDomain.ThreadSet.is_empty created then
Expand All @@ -38,7 +37,7 @@ let pretty () {tid; created; must_joined} =
else
Some (Pretty.dprintf "must_joined=%a" ConcDomain.ThreadSet.pretty must_joined)
in
let docs = List.filter_map Fun.id [tid_doc; created_doc; must_joined_doc] in
let docs = List.filter_map Fun.id [created_doc; must_joined_doc] in
Pretty.dprintf "{%a}" (Pretty.d_list "; " Pretty.insert) docs

include Printable.SimplePretty (
Expand Down
9 changes: 6 additions & 3 deletions src/cdomains/threadIdDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,10 +56,13 @@ struct
(struct let name = "no node" end))

let show = function
sim642 marked this conversation as resolved.
Show resolved Hide resolved
| (f, Some (n, i)) ->
| (f, Some (n, Some i)) ->
f.vname
^ "@" ^ (CilType.Location.show (UpdateCil.getLoc n))
^ "#" ^ Option.fold ~none:"top" ~some:string_of_int i
^ "@" ^ CilType.Location.show (UpdateCil.getLoc n)
^ "#" ^ string_of_int i
| (f, Some (n, None)) ->
f.vname
^ "@" ^ CilType.Location.show (UpdateCil.getLoc n)
| (f, None) -> f.vname

include Printable.SimpleShow (
Expand Down
13 changes: 13 additions & 0 deletions tests/regression/02-base/87-casts-dep-on-param.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
$ goblint --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] 'base' --set ana.ctx_insens[+] 'mallocWrapper' --set ana.base.privatization none --enable warn.debug 87-casts-dep-on-param.c
Option warning: Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
[Info][Unsound] Unknown address in {&i} has escaped. (87-casts-dep-on-param.c:11:3-11:11)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (87-casts-dep-on-param.c:11:3-11:11)
[Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:22)} (87-casts-dep-on-param.c:13:7-13:15)
[Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:22)} (87-casts-dep-on-param.c:14:3-14:11)
[Info][Unsound] Unknown address in {&p} has escaped. (87-casts-dep-on-param.c:17:7-17:19)
[Info][Unsound] Unknown address in {&i} has escaped. (87-casts-dep-on-param.c:17:7-17:19)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (87-casts-dep-on-param.c:17:7-17:19)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 15
dead: 0
total lines: 15
2 changes: 2 additions & 0 deletions tests/regression/02-base/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(cram
(deps (glob_files *.c)))
8 changes: 4 additions & 4 deletions tests/regression/04-mutex/01-simple_rc.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]] (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]}}, 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]] (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]}}, 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
Expand Down
12 changes: 6 additions & 6 deletions tests/regression/04-mutex/49-type-invariants.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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, [email protected]: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, [email protected]:20:3-20:40#top]}, thread:[main, [email protected]:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
write with [mhp:{created={[main, [email protected]:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
read with thread:[main, [email protected]:20:3-20:40] (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, [email protected]: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, [email protected]:20:3-20:40]}}, 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
Expand All @@ -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, [email protected]: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, [email protected]:20:3-20:40#top]}, thread:[main, [email protected]:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23)
write with [mhp:{created={[main, [email protected]:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
read with thread:[main, [email protected]:20:3-20:40] (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, [email protected]: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, [email protected]:20:3-20:40]}}, 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
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/04-mutex/77-type-nested-fields.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, [email protected]:37:3-37:40#top]}, thread:[main, [email protected]: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, [email protected]: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, [email protected]:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
write with [mhp:{created={[main, [email protected]:37:3-37:40]}}, 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, [email protected]:37:3-37:40#top]}, thread:[main, [email protected]:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
write with thread:[main, [email protected]:37:3-37:40] (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
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/04-mutex/79-type-nested-fields-deep1.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, [email protected]:42:3-42:40#top]}, thread:[main, [email protected]: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, [email protected]: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, [email protected]:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
write with [mhp:{created={[main, [email protected]:42:3-42:40]}}, 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, [email protected]:42:3-42:40#top]}, thread:[main, [email protected]:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
write with thread:[main, [email protected]:42:3-42:40] (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
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/04-mutex/80-type-nested-fields-deep2.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, [email protected]:42:3-42:40#top]}, thread:[main, [email protected]: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, [email protected]: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, [email protected]:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
write with [mhp:{created={[main, [email protected]:42:3-42:40]}}, 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, [email protected]:42:3-42:40#top]}, thread:[main, [email protected]: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, [email protected]:42:3-42:40] (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
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/04-mutex/84-distribute-fields-1.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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, [email protected]:18:3-18:40#top]}, thread:[main, [email protected]: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, [email protected]:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
write with thread:[main, [email protected]:18:3-18:40] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
write with [mhp:{created={[main, [email protected]:18:3-18:40]}}, 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, [email protected]: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, [email protected]:18:3-18:40]}}, 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
Expand Down
Loading
Loading