diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 6f923f1a4..2d01d2825 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -132,26 +132,27 @@ module PulseTransferFunctions = struct (* function pointer, etc.: skip for now *) None in - match model with - | Some model -> - L.d_printfln "Found model for call@\n" ; - model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate - | None -> ( - (* do interprocedural call then destroy objects going out of scope *) - PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; - let posts = - interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate - in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - match get_out_of_scope_object call_exp actuals flags with - | Some pvar_typ -> - L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; - posts - >>= fun posts -> - List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) - |> Result.all - | None -> - posts ) + (* do interprocedural call then destroy objects going out of scope *) + let posts = + match model with + | Some model -> + L.d_printfln "Found model for call@\n" ; + model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate + | None -> + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; + let r = interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + in + match get_out_of_scope_object call_exp actuals flags with + | Some pvar_typ -> + L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; + posts + >>= fun posts -> + List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) + |> Result.all + | None -> + posts let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0f4fa6a67..3ea4b90bd 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -194,7 +194,6 @@ module ProcNameDispatcher = struct [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip - ; -"std" &:: "function" &:: "~function" &--> Cplusplus.delete ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator=" ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index c94362634..93f93a146 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -95,7 +95,8 @@ std::function ref_capture_read_lambda_ok() { f; // reading (but not invoking) the lambda doesn't use its captured vars } -int delete_lambda_then_call_bad() { +// explicit destructor call is not modelled +int FN_delete_lambda_then_call_bad() { std::function lambda = [] { return 1; }; lambda.~function(); return lambda(); diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7665340f4..2e3e49582 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,7 +1,6 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:162:12::operator()()` here,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()()` here,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here]