[Eradicate] Allow assigning null to fields marked @InjectView to support ButterKnife.

infer/src/backend/abs.ml

@@ -1373,7 +1373,7 @@ let check_junk ?original_prop pname tenv prop =
     If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *)
 let abstract_junk ?original_prop pname tenv prop =
   Absarray.array_abstraction_performed := false;
-  check_junk ~original_prop: original_prop pname tenv prop
+  check_junk ~original_prop pname tenv prop
 
 (** Remove redundant elements in an array, and check for junk afterwards *)
 let remove_redundant_array_elements pname tenv prop =

infer/src/backend/errdesc.ml

@@ -765,11 +765,11 @@ let create_dereference_desc
     if outermost_dereference is true, stop at the outermost dereference
     (skipping e.g. outermost field access) *)
 let _explain_access
-    ?use_buckets: (use_buckets = false)
-    ?outermost_array: (outermost_array = false)
-    ?outermost_dereference: (outermost_dereference = false)
-    ?is_nullable: (is_nullable = false)
-    ?is_premature_nil: (is_premature_nil = false)
+    ?(use_buckets = false)
+    ?(outermost_array = false)
+    ?(outermost_dereference = false)
+    ?(is_nullable = false)
+    ?(is_premature_nil = false)
     deref_str prop loc =
   let rec find_outermost_dereference node e = match e with
     | Sil.Const c ->
@@ -830,9 +830,9 @@ let _explain_access
 (** Produce a description of which expression is dereferenced in the current instruction, if any.
     The subexpression to focus on is obtained by removing field and index accesses. *)
 let explain_dereference
-    ?use_buckets: (use_buckets = false)
-    ?is_nullable: (is_nullable = false)
-    ?is_premature_nil: (is_premature_nil = false)
+    ?(use_buckets = false)
+    ?(is_nullable = false)
+    ?(is_premature_nil = false)
     deref_str prop loc =
   _explain_access
     ~use_buckets ~outermost_array: false ~outermost_dereference: true ~is_nullable ~is_premature_nil

infer/src/backend/procname.ml

@@ -257,7 +257,7 @@ let java_is_static = function
   | _ -> assert false
 
 (** Prints a string of a java procname with the given level of verbosity *)
-let java_to_string ?withclass: (wc = false) j verbosity =
+let java_to_string ?(withclass = false) j verbosity =
   match verbosity with
   | VERBOSE | NON_VERBOSE ->
       (* if verbose, then package.class.method(params): rtype,
@@ -276,7 +276,7 @@ let java_to_string ?withclass: (wc = false) j verbosity =
       else return_type ^ separator ^ output
   | SIMPLE -> (* methodname(...) or without ... if there are no parameters *)
       let cls_prefix =
-        if wc then
+        if withclass then
           java_type_to_string j.classname verbosity ^ "."
         else "" in
       let params =
@@ -406,9 +406,9 @@ let to_string p =
   | OBJC_BLOCK name -> name
 
 (** Convenient representation of a procname for external tools (e.g. eclipse plugin) *)
-let to_simplified_string ?withclass: (wc = false) p =
+let to_simplified_string ?(withclass = false) p =
   match p with
-  | JAVA j -> (java_to_string ~withclass: wc j SIMPLE)
+  | JAVA j -> (java_to_string ~withclass j SIMPLE)
   | C_FUNCTION (c1, c2) | STATIC (c1, c2) ->
       to_readable_string (c1, c2) false ^ "()"
   | C_METHOD osig -> c_method_to_string osig SIMPLE

infer/src/backend/prop.ml

@@ -1662,7 +1662,7 @@ let rec prop_atom_and ?(footprint = false) (p : normal t) (a : Sil.atom) : norma
             (sub_normalize sub', pi_normalize sub' nsigma' p.pi, nsigma') in
           let (eqs_zero, nsigma'') = sigma_remove_emptylseg nsigma' in
           let p' = { p with sub = nsub'; pi = npi'; sigma = nsigma''} in
-          list_fold_left (prop_atom_and ~footprint: footprint) p' eqs_zero
+          list_fold_left (prop_atom_and ~footprint) p' eqs_zero
       | Sil.Aeq (e1, e2) when (Sil.exp_compare e1 e2 = 0) ->
           p
       | Sil.Aneq (e1, e2) ->
@@ -1697,11 +1697,11 @@ let rec prop_atom_and ?(footprint = false) (p : normal t) (a : Sil.atom) : norma
 
 (** Conjoin [exp1]=[exp2] with a symbolic heap [prop]. *)
 let conjoin_eq ?(footprint = false) exp1 exp2 prop =
-  prop_atom_and ~footprint: footprint prop (Sil.Aeq(exp1, exp2))
+  prop_atom_and ~footprint prop (Sil.Aeq(exp1, exp2))
 
 (** Conjoin [exp1!=exp2] with a symbolic heap [prop]. *)
 let conjoin_neq ?(footprint = false) exp1 exp2 prop =
-  prop_atom_and ~footprint: footprint prop (Sil.Aneq (exp1, exp2))
+  prop_atom_and ~footprint prop (Sil.Aneq (exp1, exp2))
 
 (** Return the spatial part *)
 let get_sigma (p: 'a t) : Sil.hpred list = p.sigma

infer/src/checkers/annotations.ml

@@ -127,6 +127,9 @@ let ia_is_inject ia =
     (ia_ends_with ia)
     [inject; inject_view; bind]
 
+let ia_is_inject_view ia =
+  ia_ends_with ia inject_view
+
 let ia_is_mutable ia =
   ia_ends_with ia mutable_
 

infer/src/checkers/annotations.mli

@@ -59,6 +59,7 @@ val ia_get_strict : Sil.item_annotation -> Sil.annotation option
 
 val ia_is_initializer : Sil.item_annotation -> bool
 val ia_is_inject : Sil.item_annotation -> bool
+val ia_is_inject_view : Sil.item_annotation -> bool
 val ia_is_mutable : Sil.item_annotation -> bool
 val ia_is_nullable : Sil.item_annotation -> bool
 val ia_is_nonnull : Sil.item_annotation -> bool

infer/src/checkers/eradicateChecks.ml

@@ -195,10 +195,14 @@ let check_field_assignment
     typecheck_expr node instr_ref curr_pname typestate exp_rhs
       (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in
   let should_report_nullable =
+    let field_is_inject_view () = match t_ia_opt with
+      | Some (_, ia) -> Annotations.ia_is_inject_view ia
+      | _ -> false in
     TypeAnnotation.get_value Annotations.Nullable ta_lhs = false &&
     TypeAnnotation.get_value Annotations.Nullable ta_rhs = true &&
     PatternMatch.type_is_class t_lhs &&
-    not (Ident.java_fieldname_is_outer_instance fname) in
+    not (Ident.java_fieldname_is_outer_instance fname) &&
+    not (field_is_inject_view ()) in
   let should_report_absent =
     activate_optional_present &&
     TypeAnnotation.get_value Annotations.Present ta_lhs = true &&
@@ -207,7 +211,7 @@ let check_field_assignment
   let should_report_mutable =
     let field_is_mutable () = match t_ia_opt with
       | Some (_, ia) -> Annotations.ia_is_mutable ia
-      | _ -> true in
+      | _ -> false in
     activate_field_not_mutable &&
     not (Procname.is_constructor curr_pname) &&
     not (Procname.is_class_initializer curr_pname) &&

infer/src/checkers/typeErr.ml

@@ -509,11 +509,11 @@ let report_error_now
     (Cfg.Node.get_proc_desc node)
     kind_s
     loc
-    ~advice: advice
-    ~field_name: field_name
-    ~origin_loc: origin_loc
+    ~advice
+    ~field_name
+    ~origin_loc
     ~exception_kind: (fun k d -> Exceptions.Eradicate (k, d))
-    ~always_report: always_report
+    ~always_report
     description
 
 

infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java

@@ -28,8 +28,10 @@ abstract class A {
   }
 }
 
-public class FieldNotNullable extends A {
+// for butterknife
+@interface InjectView {}
 
+public class FieldNotNullable extends A {
   @Nullable
   String x;
   String y;
@@ -362,4 +364,20 @@ class NestedFieldAccess {
     }
   }
 
+  // support assignments of null to @InjectView fields, generated by butterknife
+  class SupportButterKnife {
+     @InjectView String s;
+
+     SupportButterKnife() {
+     }
+
+     void dereferencingIsOK() {
+       int n = s.length();
+     }
+
+     void assignNullIsOK() {
+       s = null;
+     }
+  }
+
 }