diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 9f2b1293e..fbfe1f30e 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -1076,21 +1076,21 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path Invalid_res (Dereference_error (deref_error, desc, pjoin)) | None -> let split = do_split () in - (* check if a missing_fld hpred is about a hidden field *) - let hpred_missing_hidden = function - | Sil.Hpointsto (_, Sil.Estruct ([(fld, _)], _), _) - -> Typ.Fieldname.is_hidden fld + (* check if a missing_fld hpred is from a dyn language (ObjC) *) + let hpred_missing_objc_class = function + | Sil.Hpointsto (_, Sil.Estruct (_, _), Exp.Sizeof {typ}) + -> Typ.is_objc_class typ | _ -> false in (* missing fields minus hidden fields *) - let missing_fld_nohidden = - List.filter ~f:(fun hp -> not (hpred_missing_hidden hp)) missing_fld + let missing_fld_not_objc_class = + List.filter ~f:(fun hp -> not (hpred_missing_objc_class hp)) missing_fld in if not !Config.footprint && split.missing_sigma <> [] then ( L.d_strln "Implication error: missing_sigma not empty in re-execution" ; Invalid_res Missing_sigma_not_empty ) - else if not !Config.footprint && missing_fld_nohidden <> [] then ( + else if not !Config.footprint && missing_fld_not_objc_class <> [] then ( L.d_strln "Implication error: missing_fld not empty in re-execution" ; Invalid_res Missing_fld_not_empty ) else report_valid_res split diff --git a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.h b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.h index 9dc6c536a..5501c473d 100644 --- a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.h +++ b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.h @@ -13,4 +13,6 @@ @property(nullable, nonatomic, copy) NSData* metadata; +- (int)getX; + @end diff --git a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.m b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.m index 86c31fe0c..2a116503b 100644 --- a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.m +++ b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.m @@ -8,6 +8,20 @@ */ #import "A.h" -@implementation A +@implementation A { + + int _x; + NSString* _name; +} + +- (instancetype)withMetadata:(NSString*)name { + self->_x = 5; + self->_name = name; + return self; +} + +- (int)getX { + return _x; +} @end diff --git a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/B.m b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/B.m index b995a2d42..c3979a4f9 100644 --- a/infer/tests/build_systems/codetoanalyze/objc_getters_setters/B.m +++ b/infer/tests/build_systems/codetoanalyze/objc_getters_setters/B.m @@ -10,7 +10,9 @@ #import "A.h" #import "B.h" -@implementation B +@implementation B { + A* _a; +} - (int)npe_no_bad_footprint_in_getter:(A*)a { int* p = nil; @@ -23,4 +25,25 @@ a.metadata = metadata; // Doesn't crash here with Bad_footprint return *p; // NPE } + +- (instancetype)infer_field_get_spec:(NSData*)m { + A* a = [A alloc]; + [a withMetadata:m]; // Doesn't crash here with Precondition_not_met, get + // correct spec with a.x=5 + self->_a = a; + return self; +} + +- (int)npe_no_precondition_not_met:(NSData*)m { + [self infer_field_get_spec:m]; + if ([self->_a getX] == 5) { + int* p_true = nil; + return *p_true; // NPE + } else { + int* p_false = nil; + return *p_false; // no NPE, because we know the value of a._x is 5 because + // we get the correct spec in the method + // infer_field_get_spec + } +} @end diff --git a/infer/tests/build_systems/objc_getters_setters/issues.exp b/infer/tests/build_systems/objc_getters_setters/issues.exp index c13afdd14..c45316009 100644 --- a/infer/tests/build_systems/objc_getters_setters/issues.exp +++ b/infer/tests/build_systems/objc_getters_setters/issues.exp @@ -1,2 +1,3 @@ build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_bad_footprint_in_getter:, 3, NULL_DEREFERENCE, [start of procedure npe_no_bad_footprint_in_getter:] build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_bad_footprint_in_setter:andMetadata:, 3, NULL_DEREFERENCE, [start of procedure npe_no_bad_footprint_in_setter:andMetadata:] +build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_precondition_not_met:, 4, NULL_DEREFERENCE, [start of procedure npe_no_precondition_not_met:,start of procedure infer_field_get_spec:,start of procedure withMetadata:,return from a call to A_withMetadata:,return from a call to B_infer_field_get_spec:,start of procedure getX,return from a call to A_getX,Condition is true]