From 7646777f7fef4f3a284d5a1aab5d03f1fef11b5f Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 10 Sep 2015 10:57:18 -0400
Subject: [PATCH] [Infer][backend] Refactoring: adding attr_is_undef method

Summary:
Just adding a utility method to support a
future change.
---
 infer/src/backend/abs.ml     |  4 +---
 infer/src/backend/sil.ml     |  4 ++++
 infer/src/backend/sil.mli    |  2 ++
 infer/src/backend/symExec.ml | 11 +++++------
 4 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index cd4f54437..fb4431b76 100644
--- a/infer/src/backend/abs.ml
+++ b/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
-                | Some (Sil.Aundef _) -> true
-                | _ -> false in
+              let is_undefined = Option.map_default Sil.attr_is_undef false alloc_attribute in
               let resource = match Errdesc.hpred_is_open_resource prop hpred with
                 | Some res -> res
                 | None -> Sil.Rmemory Sil.Mmalloc in
diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml
index c5a1a7e09..9db6f439b 100644
--- a/infer/src/backend/sil.ml
+++ b/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
diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli
index 8230b62ab..1bb942c2c 100644
--- a/infer/src/backend/sil.mli
+++ b/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
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index d3d4be075..3597b1258 100644
--- a/infer/src/backend/symExec.ml
+++ b/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
-      | Some (Sil.Aundef _) -> true
-      | _ -> false in
+    let is_undef =
+      Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute pre receiver) 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
-    | Some (Sil.Aundef _) -> !Config.angelic_execution || !Config.optimistic_cast
-    | _ -> false
+    let is_undef =
+      Option.map_default Sil.attr_is_undef false (Prop.get_resource_undef_attribute prop n_lexp) in
+    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. *)