diff --git a/src/analyses/mHPAnalysis.ml b/src/analyses/mHPAnalysis.ml index a24dbc3cd6..e9c3364c9f 100644 --- a/src/analyses/mHPAnalysis.ml +++ b/src/analyses/mHPAnalysis.ml @@ -12,7 +12,10 @@ 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} = + GobConfig.get_bool "dbg.full-output" || + (not (ConcDomain.ThreadSet.is_empty created) || + not (ConcDomain.ThreadSet.is_empty must_joined)) end let access ctx _: MHP.t = MHP.current (Analyses.ask_of_ctx ctx) diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index 2e068329ea..34474a9705 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -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 not (GobConfig.get_bool "dbg.full-output") && UniqueCount.is_top c then + Format.dprintf "" + else + Format.dprintf "(#%s)" (UniqueCount.show c) + in + let tid = + if not (GobConfig.get_bool "dbg.full-output") && ThreadLifted.is_top t then + 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 end module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 9752a774e5..aead8b6e60 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -313,10 +313,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 not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then + "⊤" + else + I.show x.v (* TODO add ikind to output *) + let pretty () x = + if not (GobConfig.get_bool "dbg.full-output") && 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 not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then + BatPrintf.fprintf o "\n\n⊤\n\n\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 @@ -3477,9 +3489,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 Z.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 when not (GobConfig.get_bool "dbg.full-output") -> Pretty.text (Z.to_string v) + | _ -> + 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 = @@ -3575,20 +3605,17 @@ 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 us = List.unique (to_list_some x) in - match us with - | [x] -> Some x - | [] -> None - | _ -> - 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 Z.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:Z.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:Z.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 + | Some v when not (GobConfig.get_bool "dbg.full-output") -> Z.to_string v + | _ -> 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 } @@ -3698,7 +3725,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 "\n\n%s\n\n\n" (show x) + let printXml f x = + match to_int x with + | Some v when not (GobConfig.get_bool "dbg.full-output") -> BatPrintf.fprintf f "\n\n%s\n\n\n" (Z.to_string v) + | _ -> BatPrintf.fprintf f "\n\n%s\n\n\n" (show x) let invariant_ikind e ik x = match to_int x with diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 85f9a0297b..19ac502c23 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -55,19 +55,23 @@ struct (struct let name = "no index" end))) (struct let name = "no node" end)) - let show = function - | (f, Some (n, i)) -> - f.vname - ^ "@" ^ (CilType.Location.show (UpdateCil.getLoc n)) - ^ "#" ^ Option.fold ~none:"top" ~some:string_of_int i - | (f, None) -> f.vname + let show (f, ni_opt) = + let vname = f.vname in + match ni_opt with + | None -> vname + | Some (n, i_opt) -> + let vname_loc = vname ^ "@" ^ CilType.Location.show (UpdateCil.getLoc n) in + match i_opt with + | Some i -> vname_loc ^ "#" ^ string_of_int i + | None when GobConfig.get_bool "dbg.full-output" -> vname_loc ^ "#⊤" + | None -> vname_loc include Printable.SimpleShow ( struct type nonrec t = t let show = show end - ) + ) let threadinit v ~multiple: t = (v, None) @@ -128,9 +132,9 @@ struct include S let name () = "created (once)" end) (struct - include S - let name () = "created (multiple times)" - end) + include S + let name () = "created (multiple times)" + end) let is_unique (_, s) = diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml index 016a72a77e..f58b7d2e92 100644 --- a/src/cdomains/mHP.ml +++ b/src/cdomains/mHP.ml @@ -24,7 +24,12 @@ let current (ask:Queries.ask) = } let pretty () {tid; created; must_joined} = - let tid_doc = Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) in + let tid_doc = + if GobConfig.get_bool "dbg.full-output" then + Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) + else + None + in (* avoid useless empty sets in race output *) let created_doc = if ConcDomain.ThreadSet.is_empty created then diff --git a/src/config/options.schema.json b/src/config/options.schema.json index df4b1365db..2b28ffd3ab 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2038,6 +2038,12 @@ "Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.", "type": "boolean", "default": false + }, + "full-output": { + "title": "dbg.full-output", + "description": "Output abstract values, etc. with full internal details, without readability-oriented simplifications.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/tests/regression/02-base/87-casts-dep-on-param.t b/tests/regression/02-base/87-casts-dep-on-param.t new file mode 100644 index 0000000000..7149803b29 --- /dev/null +++ b/tests/regression/02-base/87-casts-dep-on-param.t @@ -0,0 +1,24 @@ + $ 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 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' | tee default-output.txt + [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:$SID)} (87-casts-dep-on-param.c:13:7-13:15) + [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (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 + + $ goblint --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] 'base' --set ana.ctx_insens[+] 'mallocWrapper' --set ana.base.privatization none --enable warn.debug --enable dbg.full-output 87-casts-dep-on-param.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:13:7-13:15) + < [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:14:3-14:11) + --- + > [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID@tid:Top Threads(#top))} (87-casts-dep-on-param.c:13:7-13:15) + > [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID@tid:Top Threads(#top))} (87-casts-dep-on-param.c:14:3-14:11) + [1] diff --git a/tests/regression/02-base/dune b/tests/regression/02-base/dune new file mode 100644 index 0000000000..23c0dd3290 --- /dev/null +++ b/tests/regression/02-base/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c))) diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t index b61650c6d3..bd0bc0e161 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 + $ goblint --enable warn.deterministic 01-simple_rc.c 2>&1 | tee default-output.txt [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 @@ -13,3 +13,18 @@ live: 12 dead: 0 total lines: 12 + + $ goblint --enable warn.deterministic --enable dbg.full-output 01-simple_rc.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,5c2,5 + < 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) + --- + > 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) + > 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) + > 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) + > 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) + [1] diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index b6c43d21bc..d757519b29 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 + $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-1.txt [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]}}, 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] (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]}}, 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 @@ -21,18 +21,18 @@ [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) [Error][Imprecise][Unsound] Function definition missing - $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c + $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-2.txt [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]}}, 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] (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]}}, 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 @@ -43,3 +43,33 @@ [Info][Imprecise] Invalidating expressions: & tmp (49-type-invariants.c:21:3-21:21) [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs --enable dbg.full-output 49-type-invariants.c > full-output-1.txt 2>&1 + + $ diff default-output-1.txt full-output-1.txt + 3,4c3,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) + < 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) + --- + > 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) + > 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) + 11c11 + < 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) + --- + > 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) + [1] + + $ 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 + + $ diff default-output-2.txt full-output-2.txt + 3,4c3,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) + < 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) + --- + > 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) + > 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) + 11c11 + < 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) + --- + > 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) + [1] diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index 0ecf051578..15559cefec 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -1,16 +1,16 @@ - $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c + $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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 @@ -24,3 +24,18 @@ [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20) [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 77-type-nested-fields.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,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) + < 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) + --- + > 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) + > 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) + 12c12 + < 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) + --- + > 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) + [1] 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..680200aecd 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -1,16 +1,16 @@ - $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c + $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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 @@ -24,3 +24,18 @@ [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20) [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 79-type-nested-fields-deep1.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (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]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + --- + > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + 12c12 + < write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + --- + > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + [1] 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..4a2811ccbd 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -1,16 +1,16 @@ - $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c + $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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 @@ -24,3 +24,18 @@ [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22) [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 80-type-nested-fields-deep2.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < write with thread:[main, t_fun@80-type-nested-fields-deep2.c: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, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + --- + > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + 12c12 + < write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + --- + > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + [1] diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t index 7c79572d88..0fd55dcb53 100644 --- a/tests/regression/04-mutex/84-distribute-fields-1.t +++ b/tests/regression/04-mutex/84-distribute-fields-1.t @@ -1,15 +1,30 @@ - $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c + $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c 2>&1 | tee default-output.txt [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] (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]}}, 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]}}, 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 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 84-distribute-fields-1.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40] (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]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + --- + > write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + 10c10 + < write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + [1] diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t index 303c10dccd..7f8fb7c942 100644 --- a/tests/regression/04-mutex/85-distribute-fields-2.t +++ b/tests/regression/04-mutex/85-distribute-fields-2.t @@ -1,15 +1,30 @@ - $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c + $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c 2>&1 | tee default-output.txt [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] (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]}}, 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]}}, 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 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 85-distribute-fields-2.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40] (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]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + --- + > write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + 10c10 + < write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + [1] diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index 084148392c..c5ebd6d28a 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -1,15 +1,30 @@ - $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c + $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c 2>&1 | tee default-output.txt [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] (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]}}, 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]}}, 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 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 86-distribute-fields-3.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40] (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]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + --- + > write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + 10c10 + < write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + [1] diff --git a/tests/regression/04-mutex/87-distribute-fields-4.t b/tests/regression/04-mutex/87-distribute-fields-4.t index 5c26e80592..2d3dfb6b7c 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 + $ goblint --enable warn.deterministic --enable allglobs 87-distribute-fields-4.c 2>&1 | tee default-output.txt [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] (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]}}, 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 @@ -11,3 +11,14 @@ live: 8 dead: 0 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 87-distribute-fields-4.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40] (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]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + --- + > write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}, thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + [1] diff --git a/tests/regression/04-mutex/88-distribute-fields-5.t b/tests/regression/04-mutex/88-distribute-fields-5.t index 8f0014e34c..0afdc729ef 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 + $ goblint --enable warn.deterministic --enable allglobs 88-distribute-fields-5.c 2>&1 | tee default-output.txt [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] (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]}}, 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 @@ -11,3 +11,14 @@ live: 8 dead: 0 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 88-distribute-fields-5.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40] (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]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + --- + > write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}, thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + [1] diff --git a/tests/regression/04-mutex/89-distribute-fields-6.t b/tests/regression/04-mutex/89-distribute-fields-6.t index aeb5050395..20533099de 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 + $ goblint --enable warn.deterministic --enable allglobs 89-distribute-fields-6.c 2>&1 | tee default-output.txt [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] (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]}}, 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 @@ -11,3 +11,14 @@ live: 8 dead: 0 total lines: 8 + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 89-distribute-fields-6.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40] (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]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + --- + > write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}, thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + [1] 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..1a5c739e9c 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -1,18 +1,18 @@ - $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c + $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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]}}, 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 @@ -26,3 +26,22 @@ [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20) [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 90-distribute-fields-type-1.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (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]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + --- + > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + 12c12 + < write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + --- + > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + 14c14 + < write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + [1] 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..e22b21d2bd 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -1,18 +1,18 @@ - $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c + $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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]}}, 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 @@ -26,3 +26,22 @@ [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17) [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 91-distribute-fields-type-2.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (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]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + --- + > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + 12c12 + < write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + --- + > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + 14c14 + < write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + [1] 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..d754ded21b 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -1,18 +1,18 @@ - $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c + $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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]}}, 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 @@ -26,3 +26,22 @@ [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20) [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 92-distribute-fields-type-deep.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 4,5c4,5 + < write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (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]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + --- + > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + 12c12 + < write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + --- + > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + 14c14 + < write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + [1] 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..7e0dc61a3c 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 + $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c 2>&1 | tee default-output.txt [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] (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]}}, 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] (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]}}, 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 @@ -22,3 +22,22 @@ [Info][Imprecise] Invalidating expressions: & tmp (93-distribute-fields-type-global.c:13:3-13:29) [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --enable allglobs --enable dbg.full-output 93-distribute-fields-type-global.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 3,4c3,4 + < read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (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]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + --- + > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + 11c11 + < read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + --- + > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + 13c13 + < write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + --- + > write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + [1] diff --git a/tests/regression/06-symbeq/14-list_entry_rc.t b/tests/regression/06-symbeq/14-list_entry_rc.t new file mode 100644 index 0000000000..0e5ec3ce9f --- /dev/null +++ b/tests/regression/06-symbeq/14-list_entry_rc.t @@ -0,0 +1,38 @@ + $ goblint --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 14-list_entry_rc.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' | tee default-output.txt + [Info][Imprecise] Invalidating expressions: & mutexattr (14-list_entry_rc.c:37:3-37:37) + [Warning][Unknown] unlocking mutex ((alloc@sid:$SID@tid:[main])[1].mutex) which may not be held (14-list_entry_rc.c:28:3-28:34) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 23 + dead: 0 + total lines: 23 + [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) + write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (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]}}, 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] (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]}}, 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 + unsafe: 1 + total memory locations: 2 + + $ goblint --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable dbg.full-output 14-list_entry_rc.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt + + $ diff default-output.txt full-output.txt + 2c2 + < [Warning][Unknown] unlocking mutex ((alloc@sid:$SID@tid:[main])[1].mutex) which may not be held (14-list_entry_rc.c:28:3-28:34) + --- + > [Warning][Unknown] unlocking mutex ((alloc@sid:$SID@tid:[main](#top))[def_exc:1].mutex) which may not be held (14-list_entry_rc.c:28:3-28:34) + 7,11c7,11 + < [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) + < write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (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]}}, 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] (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]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + --- + > [Warning][Race] Memory location (alloc@sid:$SID@tid:[main](#top))[?].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#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (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#⊤]}}, 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#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + [1] diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index b63471a45e..a5f977008d 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -1,24 +1,44 @@ Disable info messages because race summary contains (safe) memory location count, which is different on Linux and OSX. - $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 16-type_rc.c + $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 16-type_rc.c 2>&1 | tee default-output-1.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) [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] (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]}}, 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 - $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c + $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c 2>&1 | tee default-output-2.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) [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] (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 + + $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable dbg.full-output 16-type_rc.c > full-output-1.txt 2>&1 + + $ diff default-output-1.txt full-output-1.txt + 6,7c6,7 + < write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (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]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + --- + > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + [1] + + $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 16-type_rc.c > full-output-2.txt 2>&1 + + $ diff default-output-2.txt full-output-2.txt + 6c6 + < write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + --- + > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + [1] diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t index 227c66058e..90f0661f67 100644 --- a/tests/regression/06-symbeq/21-mult_accs_rc.t +++ b/tests/regression/06-symbeq/21-mult_accs_rc.t @@ -1,6 +1,6 @@ Disable info messages because race summary contains (safe) memory location count, which is different on Linux and OSX. - $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 21-mult_accs_rc.c + $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 21-mult_accs_rc.c 2>&1 | tee default-output-1.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:16:3-16:14) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:32) @@ -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] (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]}}, 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) @@ -17,7 +17,7 @@ Disable info messages because race summary contains (safe) memory location count [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14) [Error][Imprecise][Unsound] Function definition missing - $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 21-mult_accs_rc.c + $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 21-mult_accs_rc.c 2>&1 | tee default-output-2.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:14:3-14:32) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:16:3-16:14) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:17:3-17:32) @@ -25,10 +25,30 @@ 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] (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) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14) [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:27:3-27:14) [Error][Imprecise][Unsound] Function definition missing + + $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable dbg.full-output 21-mult_accs_rc.c > full-output-1.txt 2>&1 + + $ diff default-output-1.txt full-output-1.txt + 8,9c8,9 + < write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (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]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + --- + > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (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#⊤]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + [1] + + $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 21-mult_accs_rc.c > full-output-2.txt 2>&1 + + $ diff default-output-2.txt full-output-2.txt + 8c8 + < write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + --- + > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + [1] diff --git a/tests/regression/45-escape/51-fresh-global.t b/tests/regression/45-escape/51-fresh-global.t new file mode 100644 index 0000000000..ceb21425e8 --- /dev/null +++ b/tests/regression/45-escape/51-fresh-global.t @@ -0,0 +1,22 @@ + $ goblint --set ana.activated[+] mallocFresh --set ana.activated[-] mhp --set ana.thread.domain plain 51-fresh-global.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' | tee default-output.txt + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 15 + dead: 0 + total lines: 15 + [Warning][Race] Memory location (alloc@sid:$SID@tid:main) (race with conf. 110): (51-fresh-global.c:25:7-25:31) + write with lock:{A} (conf. 110) (exp: & *i) (51-fresh-global.c:10:3-10:10) + write with thread:main (conf. 110) (exp: & *i) (51-fresh-global.c:27:3-27:9) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 + + $ goblint --set ana.activated[+] mallocFresh --set ana.activated[-] mhp --set ana.thread.domain plain --enable dbg.full-output 51-fresh-global.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt + + $ diff default-output.txt full-output.txt + 5c5 + < [Warning][Race] Memory location (alloc@sid:$SID@tid:main) (race with conf. 110): (51-fresh-global.c:25:7-25:31) + --- + > [Warning][Race] Memory location (alloc@sid:$SID@tid:main(#top)) (race with conf. 110): (51-fresh-global.c:25:7-25:31) + [1] diff --git a/tests/regression/45-escape/dune b/tests/regression/45-escape/dune new file mode 100644 index 0000000000..23c0dd3290 --- /dev/null +++ b/tests/regression/45-escape/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c))) diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.c b/tests/regression/74-invalid_deref/01-oob-heap-simple.c index 10c7864184..1137e86ec6 100644 --- a/tests/regression/74-invalid_deref/01-oob-heap-simple.c +++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.c @@ -3,10 +3,12 @@ int main(int argc, char const *argv[]) { char *ptr = malloc(5 * sizeof(char)); + long r; *ptr = 'a';//NOWARN *(ptr + 1) = 'b';//NOWARN *(ptr + 10) = 'c';//WARN + *(ptr + r) = 'd';//WARN free(ptr); diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.t b/tests/regression/74-invalid_deref/01-oob-heap-simple.t new file mode 100644 index 0000000000..ac3ec99fa8 --- /dev/null +++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.t @@ -0,0 +1,19 @@ + $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval 01-oob-heap-simple.c 2>&1 | tee default-output.txt + [Warning] The memOutOfBounds analysis enables cil.addNestedScopeAttr. + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 8 + dead: 0 + total lines: 8 + + $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval --enable dbg.full-output 01-oob-heap-simple.c > full-output.txt 2>&1 + + $ diff default-output.txt full-output.txt + 2,3c2,3 + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + --- + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size ((5,[5,5])) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + [1] diff --git a/tests/regression/74-invalid_deref/dune b/tests/regression/74-invalid_deref/dune new file mode 100644 index 0000000000..23c0dd3290 --- /dev/null +++ b/tests/regression/74-invalid_deref/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c)))