[Infer][backend] Refactoring: adding attr_is_undef method

Summary:
Just adding a utility method to support a
future change.

infer/src/backend/abs.ml

@@ -1287,9 +1287,7 @@ let check_junk ?original_prop pname tenv prop =
                 list_iter do_entry entries;
                 !res in
               L.d_decrease_indent 1;
-              let is_undefined = match alloc_attribute with
+              let is_undefined = Option.map_default Sil.attr_is_undef false alloc_attribute in
-                | Some (Sil.Aundef _) -> true
-                | _ -> false in
               let resource = match Errdesc.hpred_is_open_resource prop hpred with
                 | Some res -> res
                 | None -> Sil.Rmemory Sil.Mmalloc in

infer/src/backend/sil.ml

@@ -1136,6 +1136,10 @@ let attribute_to_category att =
   | Adiv0 _ -> ACdiv0
   | Aobjc_null _ -> ACobjc_null
 
+let attr_is_undef = function
+  | Aundef _ -> true
+  | _ -> false
+
 let cname_opt_compare nameo1 nameo2 = match nameo1, nameo2 with
   | None, None -> 0
   | None, _ -> - 1

infer/src/backend/sil.mli

@@ -694,6 +694,8 @@ val attribute_category_equal : attribute_category -> attribute_category -> bool
 (**  Return the category to which the attribute belongs. *)
 val attribute_to_category : attribute -> attribute_category
 
+val attr_is_undef : attribute -> bool
+
 val const_compare : const -> const -> int
 
 val const_equal : const -> const -> bool

infer/src/backend/symExec.ml

@@ -814,9 +814,8 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc
     [(add_objc_null_attribute_or_nullify_result pre, path)]
   else
     let res = Tabulation.exe_function_call tenv cfg ret_ids pdesc callee_pname loc actual_params pre path in
-    let is_undef = match Prop.get_resource_undef_attribute pre receiver with
+    let is_undef =
-      | Some (Sil.Aundef _) -> true
+      Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute pre receiver) in
-      | _ -> false in
     if !Config.footprint && not is_undef then
       let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *)
         let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
@@ -1536,9 +1535,9 @@ module ModelBuiltins = struct
     [(prop, path)]
 
   let is_undefined_opt prop n_lexp =
-    match Prop.get_resource_undef_attribute prop n_lexp with
+    let is_undef =
-    | Some (Sil.Aundef _) -> !Config.angelic_execution || !Config.optimistic_cast
+      Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute prop n_lexp) in
-    | _ -> false
+    is_undef && (!Config.angelic_execution || !Config.optimistic_cast)
 
   (** Creates an object in the heap with a given type, when the object is not known to be null or when it doesn't
       appear already in the heap. *)