diff --git a/infer/src/IR/JavaClassName.ml b/infer/src/IR/JavaClassName.ml index 43b94e459..6bb9e2141 100644 --- a/infer/src/IR/JavaClassName.ml +++ b/infer/src/IR/JavaClassName.ml @@ -9,7 +9,8 @@ open! IStd module F = Format module L = Logging -(** invariant: if [package = Some str] then [not (String.equal str "")] *) +(** invariant: if [package = Some str] then [not (String.equal str "")]. [classname] appears first + so that the comparator fails earlier *) type t = {classname: string; package: string option} [@@deriving compare, equal] module Map = Caml.Map.Make (struct diff --git a/infer/src/IR/JavaClassName.mli b/infer/src/IR/JavaClassName.mli index 1bf993f69..f74effba1 100644 --- a/infer/src/IR/JavaClassName.mli +++ b/infer/src/IR/JavaClassName.mli @@ -14,12 +14,16 @@ module Map : Caml.Map.S with type key = t module Set : Caml.Set.S with type elt = t val make : package:string option -> classname:string -> t +(** [make ~package:(Some "java.lang") "Object"] creates a value representing [java.lang.Object] *) val from_string : string -> t +(** [from_string "java.lang.Object"] is same as [make ~package:(Some "java.lang") "Object"] *) val to_string : t -> string +(** [to_string (from_string "X.Y.Z") = "X.Y.Z"] *) val pp : Format.formatter -> t -> unit +(** [pp] includes package if any *) val pp_with_verbosity : verbose:bool -> Format.formatter -> t -> unit (** if [verbose] then print package if present, otherwise only print class *) diff --git a/infer/src/IR/JavaSplitName.ml b/infer/src/IR/JavaSplitName.ml index 3eb61564d..83921c33e 100644 --- a/infer/src/IR/JavaSplitName.ml +++ b/infer/src/IR/JavaSplitName.ml @@ -34,8 +34,6 @@ let java_lang_string = make ~package:"java.lang" "String" let java_lang_string_array = make ~package:"java.lang" "String[]" -let void = make "void" - let pp_type_verbosity ~verbose fmt = function | {package= Some package; type_name} when verbose -> F.fprintf fmt "%s.%s" package type_name diff --git a/infer/src/IR/JavaSplitName.mli b/infer/src/IR/JavaSplitName.mli index 69217a880..716848c6d 100644 --- a/infer/src/IR/JavaSplitName.mli +++ b/infer/src/IR/JavaSplitName.mli @@ -31,9 +31,6 @@ val java_lang_string : t val java_lang_string_array : t (** [java.lang.String\[\]] type *) -val void : t -(** Java [void] type *) - val package : t -> string option val type_name : t -> string diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index ffd134141..80d1f2b7e 100644 --- a/infer/src/IR/Procname.ml +++ b/infer/src/IR/Procname.ml @@ -25,14 +25,12 @@ module Java = struct (* TODO: use Mangled.t here *) type java_type = JavaSplitName.t [@@deriving compare, equal] - let java_void = JavaSplitName.void - (** Type of java procedure names. *) type t = { method_name: string ; parameters: java_type list ; class_name: Typ.Name.t - ; return_type: java_type option (* option because constructors have no return type *) + ; return_type: Typ.t option (* option because constructors have no return type *) ; kind: kind } [@@deriving compare] @@ -40,9 +38,7 @@ module Java = struct {class_name; return_type; method_name; parameters; kind} - let pp_return_type ~verbose fmt j = - Option.iter j.return_type ~f:(JavaSplitName.pp_type_verbosity ~verbose fmt) - + let pp_return_type ~verbose fmt j = Option.iter j.return_type ~f:(Typ.pp_java ~verbose fmt) let constructor_method_name = "" @@ -111,34 +107,7 @@ module Java = struct F.fprintf fmt "%a(%s)" pp_method_name j params - let get_return_typ pname_java = - let rec java_from_string = function - | "" | "void" -> - Typ.void - | "int" -> - Typ.int - | "byte" -> - Typ.java_byte - | "short" -> - Typ.java_short - | "boolean" -> - Typ.boolean - | "char" -> - Typ.java_char - | "long" -> - Typ.long - | "float" -> - Typ.float - | "double" -> - Typ.double - | typ_str when String.contains typ_str '[' -> - let stripped_typ = String.sub typ_str ~pos:0 ~len:(String.length typ_str - 2) in - Typ.(mk_ptr (mk_array (java_from_string stripped_typ))) - | typ_str -> - Typ.(mk_ptr (mk_struct (Typ.Name.Java.from_string typ_str))) - in - java_from_string (F.asprintf "%a" (pp_return_type ~verbose:true) pname_java) - + let get_return_typ pname_java = Option.value ~default:Typ.void pname_java.return_type let is_close {method_name} = String.equal method_name "close" @@ -148,7 +117,7 @@ module Java = struct { method_name= class_initializer_method_name ; parameters= [] ; class_name - ; return_type= Some java_void + ; return_type= Some Typ.void ; kind= Static } diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index 51332e8a5..0d118bd1a 100644 --- a/infer/src/IR/Procname.mli +++ b/infer/src/IR/Procname.mli @@ -31,7 +31,7 @@ module Java : sig val replace_parameters : java_type list -> t -> t (** Replace the parameters of a java procname. *) - val replace_return_type : java_type -> t -> t + val replace_return_type : Typ.t -> t -> t (** Replace the method of a java procname. *) val get_class_name : t -> string @@ -254,7 +254,7 @@ end val make_java : class_name:Typ.Name.t - -> return_type:Java.java_type option + -> return_type:Typ.t option -> method_name:string -> parameters:Java.java_type list -> kind:Java.kind diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index facfddb3e..747457af4 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -590,3 +590,44 @@ let has_block_prefix s = type typ = t + +let rec pp_java ~verbose f {desc} = + let string_of_int = function + | IInt -> + JConfig.int_st + | IBool -> + JConfig.boolean_st + | ISChar -> + JConfig.byte_st + | IUShort -> + JConfig.char_st + | ILong -> + JConfig.long_st + | IShort -> + JConfig.short_st + | _ -> + L.die InternalError "pp_java int" + in + let string_of_float = function + | FFloat -> + JConfig.float_st + | FDouble -> + JConfig.double_st + | _ -> + L.die InternalError "pp_java float" + in + match desc with + | Tint ik -> + F.pp_print_string f (string_of_int ik) + | Tfloat fk -> + F.pp_print_string f (string_of_float fk) + | Tvoid -> + F.pp_print_string f JConfig.void + | Tptr (typ, _) -> + pp_java ~verbose f typ + | Tstruct (JavaClass java_class_name) -> + JavaClassName.pp_with_verbosity ~verbose f java_class_name + | Tarray {elt} -> + F.fprintf f "%a[]" (pp_java ~verbose) elt + | _ -> + L.die InternalError "pp_java rec" diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 375f56160..8a8e4b32c 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -290,6 +290,9 @@ val pp_full : Pp.env -> F.formatter -> t -> unit val pp : Pp.env -> F.formatter -> t -> unit (** Pretty print a type. *) +val pp_java : verbose:bool -> F.formatter -> t -> unit +(** Pretty print a Java type. Raises if type isn't produced by the Java frontend *) + val to_string : t -> string val d_full : t -> unit diff --git a/infer/src/java/jConfig.ml b/infer/src/IR/jConfig.ml similarity index 100% rename from infer/src/java/jConfig.ml rename to infer/src/IR/jConfig.ml diff --git a/infer/src/java/jConfig.mli b/infer/src/IR/jConfig.mli similarity index 100% rename from infer/src/java/jConfig.mli rename to infer/src/IR/jConfig.mli diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 40a5159c1..d1cd4ac87 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1099,9 +1099,10 @@ module JavaClass = struct | Exp.Const (Const.Cclass name) -> ( let enum_values_pname = let class_name_str = Ident.name_to_string name in + let class_name = Typ.JavaClass (JavaClassName.from_string class_name_str) in Procname.make_java ~class_name:(Typ.Name.Java.from_string class_name_str) - ~return_type:(Some (JavaSplitName.make (class_name_str ^ "[]"))) + ~return_type:(Some Typ.(mk_ptr (mk_array (mk_ptr (mk_struct class_name))))) ~method_name:"values" ~parameters:[] ~kind:Procname.Java.Static () in match get_summary enum_values_pname with diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 3f8a4d415..32b7a99dc 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -168,9 +168,9 @@ let method_signature_names ms = | None when String.equal method_name JConfig.constructor_name -> None | None -> - Some (JavaSplitName.make JConfig.void) + Some Typ.void | Some vt -> - Some (vt_to_java_type vt) + Some (get_named_type vt) in let args_types = List.map ~f:vt_to_java_type (JBasics.ms_args ms) in (return_type_name, method_name, args_types) diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 6f7df7693..c412bec0d 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -627,6 +627,8 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_ typestate' +let object_typ = Typ.(mk_ptr (mk_struct Name.Java.java_lang_object)) + (* Handle m.put(k,v) as assignment pvar = v for the pvar associated to m.get(k) *) let do_map_put ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as analysis_data) call_params callee_pname loc node calls_this checks instr_ref ~nullsafe_mode @@ -637,7 +639,7 @@ let do_map_put ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as anal let parameters = [object_t] in pname_put |> Procname.Java.replace_method_name "get" - |> Procname.Java.replace_return_type object_t + |> Procname.Java.replace_return_type object_typ |> Procname.Java.replace_parameters parameters in match call_params with @@ -813,10 +815,9 @@ let rec check_condition_for_sil_prune (DExp.Dretcall (DExp.Dconst (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) -> let pname_java' = - let object_t = JavaSplitName.java_lang_object in pname_java |> Procname.Java.replace_method_name "get" - |> Procname.Java.replace_return_type object_t + |> Procname.Java.replace_return_type object_typ in let fun_dexp = DExp.Dconst (Const.Cfun (Procname.Java pname_java')) in Some (DExp.Dretcall (fun_dexp, args, loc, call_flags)) diff --git a/infer/src/test_determinator/JProcname.ml b/infer/src/test_determinator/JProcname.ml index 7803694c9..529fa9fbe 100644 --- a/infer/src/test_determinator/JProcname.ml +++ b/infer/src/test_determinator/JProcname.ml @@ -98,6 +98,34 @@ module JNI = struct L.(die UserError "Cannot express a method as a Procname.Java.java_type") + let rec to_typ jni = + match jni with + | Boolean -> + Typ.boolean + | Byte -> + Typ.java_byte + | Char -> + Typ.java_char + | Short -> + Typ.java_short + | Int -> + Typ.int + | Long -> + Typ.long + | Float -> + Typ.float + | Double -> + Typ.double + | Void -> + Typ.void + | FullyQualifiedClass (pkg, classname) -> + Typ.(mk_ptr (mk_struct (JavaClass (JavaClassName.make ~package:(Some pkg) ~classname)))) + | Array typ -> + Typ.mk_ptr (Typ.mk_array (to_typ typ)) + | Method _ -> + L.die UserError "JNI: Cannot express a method as a typ" + + let tokenize input = let rec tokenize_aux input acc = match input with @@ -267,7 +295,7 @@ let create_procname ~classname ~methodname:method_name ~signature ~use_signature String.equal method_name Procname.Java.constructor_method_name || String.equal method_name Procname.Java.class_initializer_method_name then None - else Some (JNI.to_java_type return_type) + else Some (JNI.to_typ return_type) in Procname.make_java ~class_name ~return_type ~method_name ~parameters ~kind:Procname.Java.Non_Static () diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml index a7e097f50..f5e9f2b2d 100644 --- a/infer/src/topl/ToplUtils.ml +++ b/infer/src/topl/ToplUtils.ml @@ -18,7 +18,7 @@ let topl_class_typ = Typ.mk (Tstruct topl_class_name) let topl_call ret_id (ret_typ : Typ.desc) loc method_name arg_ts : Sil.instr = let e_fun = - let return_type = Some JavaSplitName.void in + let return_type = Some Typ.void in let parameters = List.map arg_ts ~f:(fun _ -> JavaSplitName.java_lang_object) in Exp.Const (Const.Cfun diff --git a/infer/src/unit/JavaProfilerSamplesTest.ml b/infer/src/unit/JavaProfilerSamplesTest.ml index 08aa87bf7..e5e45865a 100644 --- a/infer/src/unit/JavaProfilerSamplesTest.ml +++ b/infer/src/unit/JavaProfilerSamplesTest.ml @@ -202,7 +202,7 @@ let test_from_json_string_with_valid_input = [ Procname.( make_java ~class_name:(Typ.Name.Java.from_string "ddd.eee.Fff") - ~return_type:(Some (mk_split (None, "char[][]"))) + ~return_type:(Some Typ.(mk_ptr (mk_array (mk_ptr (mk_array java_char))))) ~method_name:"methodTwo" ~parameters: [ mk_split (Some "java.lang", "String") @@ -212,8 +212,8 @@ let test_from_json_string_with_valid_input = ; Procname.( make_java ~class_name:(Typ.Name.Java.from_string "aaa.bbb.Ccc") - ~return_type:(Some (mk_split (None, "void"))) - ~method_name:"methodOne" ~parameters:[] ~kind:Java.Non_Static ()) ] ) ] + ~return_type:(Some Typ.void) ~method_name:"methodOne" ~parameters:[] + ~kind:Java.Non_Static ()) ] ) ] in let expected3 = [ ( "label1" @@ -233,13 +233,13 @@ let test_from_json_string_with_valid_input = [ Procname.( make_java ~class_name:(Typ.Name.Java.from_string "ddd.eee.Fff") - ~return_type:(Some (mk_split (None, "void"))) - ~method_name:"methodTwo" ~parameters:[] ~kind:Java.Non_Static ()) + ~return_type:(Some Typ.void) ~method_name:"methodTwo" ~parameters:[] + ~kind:Java.Non_Static ()) ; Procname.( make_java ~class_name:(Typ.Name.Java.from_string "aaa.bbb.Ccc") - ~return_type:(Some (mk_split (None, "void"))) - ~method_name:"methodOne" ~parameters:[] ~kind:Java.Non_Static ()) ] ) ] + ~return_type:(Some Typ.void) ~method_name:"methodOne" ~parameters:[] + ~kind:Java.Non_Static ()) ] ) ] in [ ("test_from_json_string_1", input1, expected1, true) ; ("test_from_json_string_2", input2, expected2, true) diff --git a/infer/tests/build_systems/racerd_dedup/issues.exp b/infer/tests/build_systems/racerd_dedup/issues.exp index 98f0c81d1..1cb70980a 100644 --- a/infer/tests/build_systems/racerd_dedup/issues.exp +++ b/infer/tests/build_systems/racerd_dedup/issues.exp @@ -2,7 +2,7 @@ DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, TH DeDup.java, build_systems.threadsafety.DeDup.separate_write_to_colocated_read():void, 68, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.colocated_read`] DeDup.java, build_systems.threadsafety.DeDup.twoWritesOneInCaller():void, 50, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void DeDup.writeToField(),access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_fields():void, 20, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void DeDup.foo(),access to `this.fielda`] -DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 37, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void DeDup.writeToField(),access to `this.field`] +DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 37, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 30, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.field`] -DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 45, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void DeDup.writeToField(),access to `this.field`] +DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 45, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,access to `this.field`] diff --git a/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java b/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java index 6d9ad5c22..783ec4c38 100644 --- a/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java +++ b/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java @@ -34,7 +34,7 @@ public class ReaderLeaks { } } - public void readerClosed_FP() throws IOException { + public void readerClosedOk() throws IOException { Reader r = null; try { r = new FileReader("testing.txt"); diff --git a/infer/tests/codetoanalyze/java/biabduction/issues.exp b/infer/tests/codetoanalyze/java/biabduction/issues.exp index 56d6c5f7e..3b2459e48 100644 --- a/infer/tests/codetoanalyze/java/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/java/biabduction/issues.exp @@ -137,7 +137,6 @@ codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.Reader codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConnect(java.io.PipedWriter):void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConnect(...),exception java.io.IOException] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConstructedWithWriter():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConstructedWithWriter(),exception java.io.IOException] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pushbackReaderNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pushbackReaderNotClosedAfterRead(),Skipping PushbackReader(...): unknown method,exception java.io.IOException] -codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerClosed_FP():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerClosed_FP(),Skipping FileReader(...): unknown method,exception java.io.IOException,Switch condition is true. Entering switch case,Taking true branch] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerNotClosedAfterRead(),Skipping FileReader(...): unknown method,exception java.io.IOException] codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.NoResourceLeakWarningAfterCheckState(java.io.File,int):void, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure NoResourceLeakWarningAfterCheckState(...),Taking false branch] codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.activityObtainTypedArrayAndLeak(android.app.Activity):void, 2, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure activityObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(TypedArray)] diff --git a/infer/tests/codetoanalyze/java/racerd/Ownership.java b/infer/tests/codetoanalyze/java/racerd/Ownership.java index b74dfd378..7d21f25cb 100644 --- a/infer/tests/codetoanalyze/java/racerd/Ownership.java +++ b/infer/tests/codetoanalyze/java/racerd/Ownership.java @@ -176,13 +176,6 @@ public class Ownership { writeToFormal(o); } - public void writeToOwnedInCalleeOk2() { - synchronized (this) { - this.field = new Obj(); - } - writeToFormal(this.field); - } - public void writeToOwnedInCalleeIndirectOk1() { Obj o = new Obj(); callWriteToFormal(o); diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index a725ffe26..aefca4a27 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -76,16 +76,15 @@ codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.unownedR codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.useLockInCalleeBad():void, 221, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.(codetoanalyze.java.checkers.Obj,java.lang.Object), 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `obj.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.cantOwnThisBad():void, 171, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.setField(Obj),access to `this.field`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 233, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(codetoanalyze.java.checkers.Obj):void, 421, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 428, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void Ownership.setField(Obj),access to `this.field`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 226, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(codetoanalyze.java.checkers.Obj):void, 414, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 421, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,call to void Ownership.setField(Obj),access to `this.field`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.ownInOneBranchBad(codetoanalyze.java.checkers.Obj,boolean):void, 82, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 403, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `checkers.Ownership.global`,,access to `checkers.Ownership.global`] +codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 396, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `checkers.Ownership.global`,,access to `checkers.Ownership.global`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.g`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 88, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `formal.g`,,access to `formal.g`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad1(codetoanalyze.java.checkers.Obj):void, 157, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad3(codetoanalyze.java.checkers.Obj):void, 166, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `o.f`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToOwnedInCalleeOk2():void, 183, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.field`,,access to `this.field`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional2_bad(boolean):void, 130, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditionalMainThreadWriteBad():void, 219, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void RaceWithMainThread.conditionalMainThreadWrite2(boolean),access to `this.mOnlyWrittenOnMain`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad():void, 152, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.ff`]