diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 86b63b1d3..2898410eb 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -60,7 +60,7 @@ exception Custom_error of string * Localise.error_desc exception Dummy_exception of Localise.error_desc exception - Dangling_pointer_dereference of PredSymb.dangling_kind option * Localise.error_desc * L.ocaml_pos + Dangling_pointer_dereference of bool (* is it user visible? *) * Localise.error_desc * L.ocaml_pos exception Deallocate_stack_variable of Localise.error_desc @@ -256,14 +256,8 @@ let recognize_exception exn = ; visibility= Exn_developer ; severity= Some Info ; category= Checker } - | Dangling_pointer_dereference (dko, desc, ocaml_pos) -> - let visibility = - match dko with - | Some _ -> - Exn_user (* only show to the user if the category was identified *) - | None -> - Exn_developer - in + | Dangling_pointer_dereference (user_visible, desc, ocaml_pos) -> + let visibility = if user_visible then Exn_user else Exn_developer in { name= IssueType.dangling_pointer_dereference ; description= desc ; ocaml_pos= Some ocaml_pos diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 0d7172cbc..1c6d86b2a 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -61,7 +61,7 @@ exception Dummy_exception of Localise.error_desc exception Dangling_pointer_dereference of - PredSymb.dangling_kind option * Localise.error_desc * Logging.ocaml_pos + bool (* is it user visible? *) * Localise.error_desc * Logging.ocaml_pos exception Deallocate_stack_variable of Localise.error_desc diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index c25cd1bc9..d58e679c9 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -451,7 +451,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst : let err_desc = Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc_exn ()) in - raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ; + raise (Exceptions.Dangling_pointer_dereference (false, err_desc, __POS__)) ) ; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in let subtype = match !Language.curr_language with Clang -> Subtype.exact | Java -> Subtype.subtypes @@ -1598,7 +1598,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = | Some (Apred (Adangling dk, _)) -> let deref_str = Localise.deref_str_dangling (Some dk) in let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc_exn ()) in - raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) + raise (Exceptions.Dangling_pointer_dereference (true, err_desc, __POS__)) | Some (Apred (Aundef _, _)) -> () | Some (Apred (Aresource ({ra_kind= Rrelease} as ra), _)) -> @@ -1609,7 +1609,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = if Prover.check_equal tenv Prop.prop_emp (Exp.root_of_lexp root) Exp.minus_one then let deref_str = Localise.deref_str_dangling None in let err_desc = Errdesc.explain_dereference pname tenv deref_str prop loc in - raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) + raise (Exceptions.Dangling_pointer_dereference (false, err_desc, __POS__)) (* Check that an expression representin an objc block can be null and raise a [B1] null exception.*) diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 3bc82c4c1..db41fbb8a 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -1076,7 +1076,7 @@ let check_uninitialize_dangling_deref caller_pname tenv callee_pname actual_pre ~f:(fun (p, _) -> match check_dereferences caller_pname tenv callee_pname actual_pre sub p formal_params with | Some (Deref_undef_exp, desc) -> - raise (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAuninit, desc, __POS__)) + raise (Exceptions.Dangling_pointer_dereference (true, desc, __POS__)) | _ -> () ) props @@ -1333,13 +1333,11 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re | Dereference_error (Deref_minusone, desc, path_opt) -> trace_call CR_not_met ; extend_path path_opt None ; - raise - (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAminusone, desc, __POS__)) + raise (Exceptions.Dangling_pointer_dereference (true, desc, __POS__)) | Dereference_error (Deref_undef_exp, desc, path_opt) -> trace_call CR_not_met ; extend_path path_opt None ; - raise - (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAuninit, desc, __POS__)) + raise (Exceptions.Dangling_pointer_dereference (true, desc, __POS__)) | Dereference_error (Deref_null pos, desc, path_opt) -> trace_call CR_not_met ; extend_path path_opt (Some pos) ;