From 86f52e52edc82815b9f1febbe7d72a5b9559d8a0 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Tue, 6 Nov 2018 08:19:45 -0800 Subject: [PATCH] [pulse] Operator= copy assignment Summary: For a general case of `operator=` we want to create a fresh location for the first parameter as `operator=` behaves as copy assignment. Reviewed By: jvillard Differential Revision: D12940635 fbshipit-source-id: 89c6e530d --- infer/src/checkers/Pulse.ml | 6 ++++++ infer/tests/codetoanalyze/cpp/pulse/issues.exp | 12 ++++++------ .../codetoanalyze/cpp/pulse/use_after_destructor.cpp | 8 ++++++++ 3 files changed, 20 insertions(+), 6 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 420cc0d95..c72a474c1 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -83,6 +83,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct when Var.is_cpp_temporary (fst rhs_base) -> let lhs_deref = AccessExpression.dereference lhs in exec_assign lhs_deref rhs_exp call_loc astate + (* copy assignment *) + | [AccessExpression lhs; HilExp.AccessExpression rhs] -> + let lhs_deref = AccessExpression.dereference lhs in + let rhs_deref = AccessExpression.dereference rhs in + PulseDomain.havoc call_loc lhs_deref astate + >>= fun astate -> PulseDomain.read call_loc rhs_deref astate >>| fst | _ -> read_all actuals astate ) | _ -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index fd820a2bc..52b4e508a 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -10,12 +10,12 @@ 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 102, column 3 here,accessed `s->f` 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] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 149, column 3 here,accessed `alias` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, column 3 here,accessed `pc->f` 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 62, 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 140, 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 148, column 3 here,accessed `alias` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 157, column 3 here,accessed `alias` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 69, column 3 here,accessed `*(s.f)` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 202, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 351060373..47f325de2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -36,6 +36,14 @@ int reinit_after_explicit_destructor_ok() { return *s.f; } +int reinit_after_explicit_destructor2_ok() { + S s(1); + S s2(2); + s.~S(); + s = s2; + return *s.f; +} + void placement_new_explicit_destructor_ok() { char buf[sizeof(S)]; {