diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 52b6d1f28..0298ba8ef 100644 --- a/infer/src/backend/prop.ml +++ b/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 *) diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index ed8115ea1..d9f5ebc4c 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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]