diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 337ffda5b..a000b1f39 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -41,6 +41,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct false + let exec_assign lhs_access (rhs_exp : HilExp.t) loc astate = + (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) + match rhs_exp with + | AccessExpression rhs_access -> + PulseDomain.read loc rhs_access astate + >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate + | Constant (Cint address) when IntLit.iszero address -> + PulseDomain.write loc lhs_access PulseDomain.AbstractAddress.nullptr astate + | _ -> + PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate + >>= PulseDomain.havoc loc lhs_access + + let exec_call _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = let read_all args astate = PulseDomain.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate @@ -62,6 +75,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct PulseDomain.havoc call_loc constructed_object astate >>= read_all rest | _ -> Ok astate ) + | Direct (Typ.Procname.ObjC_Cpp callee_pname) + when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> ( + match actuals with + (* We want to assign *lhs to *rhs when rhs is materialized temporary created in constructor *) + | [AccessExpression lhs; (HilExp.AccessExpression (AddressOf (Base rhs_base)) as rhs_exp)] + when Var.is_cpp_temporary (fst rhs_base) -> + let lhs_deref = AccessExpression.dereference lhs in + exec_assign lhs_deref rhs_exp call_loc astate + | _ -> + read_all actuals astate ) | _ -> read_all actuals astate @@ -86,19 +109,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct = match instr with | Assign (lhs_access, rhs_exp, loc) -> - (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) - let result = - match rhs_exp with - | AccessExpression rhs_access -> - PulseDomain.read loc rhs_access astate - >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate - | Constant (Cint address) when IntLit.iszero address -> - PulseDomain.write loc lhs_access PulseDomain.AbstractAddress.nullptr astate - | _ -> - PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate - >>= PulseDomain.havoc loc lhs_access - in - check_error summary result + exec_assign lhs_access rhs_exp loc astate |> check_error summary | Assume (condition, _, _, loc) -> PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 63b1d71d1..97f83e3fa 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -7,7 +7,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 103, column 3 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 34, column 3 here,accessed `&(s)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 54, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 132, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 140, column 3 here,accessed `alias` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 67d3df978..351060373 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -29,7 +29,7 @@ void nested_scope_destructor_ok() { { S s(1); } } -int FP_reinit_after_explicit_destructor_ok() { +int reinit_after_explicit_destructor_ok() { S s(1); s.~S(); s = S(2);