diff --git a/infer/src/IR/CallFlags.ml b/infer/src/IR/CallFlags.ml index c4933b771..dc27fe2da 100644 --- a/infer/src/IR/CallFlags.ml +++ b/infer/src/IR/CallFlags.ml @@ -17,7 +17,6 @@ type t = ; cf_injected_destructor: bool ; cf_interface: bool ; cf_is_objc_block: bool - ; cf_noreturn: bool ; cf_virtual: bool ; cf_with_block_parameters: bool } [@@deriving compare] @@ -27,14 +26,12 @@ let pp f ; cf_injected_destructor ; cf_interface ; cf_is_objc_block - ; cf_noreturn ; cf_with_block_parameters ; cf_virtual }[@warning "+9"]) = if cf_assign_last_arg then F.pp_print_string f " assign_last" ; if cf_injected_destructor then F.pp_print_string f " injected" ; if cf_interface then F.pp_print_string f " interface" ; if cf_is_objc_block then F.pp_print_string f " objc_block" ; - if cf_noreturn then F.pp_print_string f " noreturn" ; if cf_with_block_parameters then F.pp_print_string f " block_params" ; if cf_virtual then F.pp_print_string f " virtual" ; () @@ -45,6 +42,5 @@ let default = ; cf_injected_destructor= false ; cf_interface= false ; cf_is_objc_block= false - ; cf_noreturn= false ; cf_with_block_parameters= false ; cf_virtual= false } diff --git a/infer/src/IR/CallFlags.mli b/infer/src/IR/CallFlags.mli index 67e4b2a5a..57ad7a5d3 100644 --- a/infer/src/IR/CallFlags.mli +++ b/infer/src/IR/CallFlags.mli @@ -18,7 +18,6 @@ type t = (** true if this is an implicit C++ destructor call injected by the clang frontend *) ; cf_interface: bool ; cf_is_objc_block: bool - ; cf_noreturn: bool ; cf_virtual: bool ; cf_with_block_parameters: bool } [@@deriving compare] diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 5a05ef0d2..4b4309ec7 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -217,8 +217,6 @@ module NoReturn = struct Procdesc.Node.get_instrs node |> Instrs.exists ~f:(fun (instr : Sil.instr) -> match instr with - | Call (_, _, _, _, {cf_noreturn= true}) -> - true | Call (_, Const (Cfun proc_name), _, _, _) -> ( match Attributes.load proc_name with | Some {ProcAttributes.is_no_return= true} -> diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index b721ad29c..a1163a6f3 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1476,29 +1476,23 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t && not (Rearrange.is_only_pt_by_fld_or_param_nonnull current_pdesc tenv prop_r fun_exp) then Rearrange.check_call_to_objc_block_error tenv current_pdesc prop_r fun_exp loc ; Rearrange.check_dereference_error tenv current_pdesc prop_r fun_exp loc ; - if call_flags.CallFlags.cf_noreturn then ( - L.d_str "Unknown function pointer with noreturn attribute " ; - Sil.d_exp fun_exp ; - L.d_strln ", diverging." ; - diverge prop_r path ) - else ( - L.d_str "Unknown function pointer " ; - Sil.d_exp fun_exp ; - L.d_strln ", returning undefined value." ; - let callee_pname = Typ.Procname.from_string_c_fun "__function_pointer__" in - unknown_or_scan_call ~is_scan:false ~reason:"unresolved function pointer" (snd ret_id_typ) - Annot.Item.empty - Builtin. - { summary= current_summary - ; instr - ; tenv - ; prop_= prop_r - ; path - ; ret_id_typ - ; args= n_actual_params - ; proc_name= callee_pname - ; loc - ; exe_env } ) + L.d_str "Unknown function pointer " ; + Sil.d_exp fun_exp ; + L.d_strln ", returning undefined value." ; + let callee_pname = Typ.Procname.from_string_c_fun "__function_pointer__" in + unknown_or_scan_call ~is_scan:false ~reason:"unresolved function pointer" (snd ret_id_typ) + Annot.Item.empty + Builtin. + { summary= current_summary + ; instr + ; tenv + ; prop_= prop_r + ; path + ; ret_id_typ + ; args= n_actual_params + ; proc_name= callee_pname + ; loc + ; exe_env } | Sil.Metadata (Nullify (pvar, _)) -> ( let eprop = Prop.expose prop_ in match diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 5a922898e..3b8071038 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -110,7 +110,7 @@ module PulseTransferFunctions = struct let model = match proc_name_of_call call_exp with | Some callee_pname -> - PulseModels.dispatch tenv callee_pname flags + PulseModels.dispatch tenv callee_pname | None -> (* function pointer, etc.: skip for now *) None diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 7a9b58476..fc50dd9b5 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -296,13 +296,9 @@ let builtins_dispatcher = fun proc_name -> Hashtbl.find builtins_map proc_name -let dispatch tenv proc_name flags = +let dispatch tenv proc_name = match builtins_dispatcher proc_name with | Some _ as result -> result - | None -> ( - match ProcNameDispatcher.dispatch tenv proc_name with - | Some _ as result -> - result - | None -> - if flags.CallFlags.cf_noreturn then Some Misc.early_exit else None ) + | None -> + ProcNameDispatcher.dispatch tenv proc_name diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index ac0589781..a71b6b4f0 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -17,4 +17,4 @@ type exec_fun = type model = exec_fun -val dispatch : Tenv.t -> Typ.Procname.t -> CallFlags.t -> model option +val dispatch : Tenv.t -> Typ.Procname.t -> model option