From bc799fc6cd47a1bab5dee06977b5b68f0c1cfa91 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 18 Dec 2019 09:32:57 -0800 Subject: [PATCH] [IR] `PredSymb.dangling_kind option` can be replaced by `bool` Summary: This one is just for fun. Reviewed By: ngorogiannis Differential Revision: D19158529 fbshipit-source-id: 2ccda60ca --- infer/src/IR/Exceptions.ml | 12 +++--------- infer/src/IR/Exceptions.mli | 2 +- infer/src/biabduction/Rearrange.ml | 6 +++--- infer/src/biabduction/Tabulation.ml | 8 +++----- 4 files changed, 10 insertions(+), 18 deletions(-) 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) ;