[infer][biabduction] no longer drop the atoms that are referring to footprint variables

Summary: Atoms of the form `identifier = footprint var` naturally occurs with the angelic analysis mode. So it is not clear to me why we should drop those.

Reviewed By: sblackshear

Differential Revision: D5654754

fbshipit-source-id: 9dd2eb5

infer/src/backend/prop.ml

@@ -219,8 +219,8 @@ let pi_of_subst sub = List.map ~f:(fun (id1, e2) -> Sil.Aeq (Var id1, e2)) (Sil.
 (** Return the pure part of [prop]. *)
 let get_pure (p: 'a t) : pi = pi_of_subst p.sub @ p.pi
 
-(* Same with get_pure, except that when we have both "x = t" and "y = t" where t is a primed ident, 
-* we add "x = y" to the result. This is crucial for the normalizer, as it tend to drop "x = t" before 
+(* Same with get_pure, except that when we have both "x = t" and "y = t" where t is a primed ident,
+* we add "x = y" to the result. This is crucial for the normalizer, as it tend to drop "x = t" before
 * processing "y = t". If we don't explicitly preserve "x = y", the normalizer cannot pick it up *)
 let get_pure_extended p =
   let base = get_pure p in
@@ -1653,15 +1653,8 @@ module Normalize = struct
       in
       if not footprint then p'
       else
-        let fav_a' = Sil.atom_fav a' in
-        let fav_nofootprint_a' =
-          Sil.fav_copy_filter_ident fav_a' (fun id -> not (Ident.is_footprint id))
-        in
-        let predicate_warning = not (Sil.fav_is_empty fav_nofootprint_a') in
         let p'' =
-          if predicate_warning then footprint_normalize tenv p'
-          else
-            match a' with
+          match a' with
             | Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e)
              -> let mysub = Sil.subst_of_list [(i, e)] in
                 let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
@@ -1670,8 +1663,6 @@ module Normalize = struct
             | _
              -> footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
         in
-        if predicate_warning then (
-          L.d_warning "dropping non-footprint " ; Sil.d_atom a' ; L.d_ln () ) ;
         unsafe_cast_to_normal p''
 
   (** normalize a prop *)

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -34,7 +34,7 @@ codetoanalyze/objc/shared/block/block_no_args.m, My_manager_m, 10, NULL_DEREFERE
 codetoanalyze/objc/shared/block/block_release.m, My_manager_blockReleaseTODO, 5, MEMORY_LEAK, [start of procedure blockReleaseTODO]
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 2, MEMORY_LEAK, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: function or method not found]
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 3, MEMORY_LEAK, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: function or method not found]
-codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, [start of procedure init]
+codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, [start of procedure init,start of procedure init,return from a call to BSuper_init]
 codetoanalyze/objc/shared/field_superclass/SuperExample.m, super_example_main, 2, MEMORY_LEAK, [start of procedure super_example_main(),Skipping init: function or method not found]
 codetoanalyze/objc/shared/memory_leaks_benchmark/RetainReleaseExample2.m, test3, 0, MEMORY_LEAK, [start of procedure test3(),start of procedure retain_release2_test(),start of procedure init,return from a call to RR2_init,return from a call to retain_release2_test]
 codetoanalyze/objc/shared/memory_leaks_benchmark/RetainReleaseExample2.m, test4, 3, MEMORY_LEAK, [start of procedure test4(),start of procedure retain_release2_test(),start of procedure init,return from a call to RR2_init,return from a call to retain_release2_test]