diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index cc1aec51b..7cac412b8 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -46,9 +46,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Direct callee_pname when is_destructor callee_pname -> ( match actuals with | [AccessExpression destroyed_access] -> + let destroyed_object = + AccessExpression.normalize (AccessExpression.Dereference destroyed_access) + in PulseDomain.invalidate - (CppDestructor (callee_pname, destroyed_access, call_loc)) - call_loc destroyed_access astate + (CppDestructor (callee_pname, destroyed_object, call_loc)) + call_loc destroyed_object astate | _ -> Ok astate ) | _ -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp index 6c06cd2e6..b7cb80546 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp @@ -73,7 +73,7 @@ int multiple_invalidations_loop_bad(int n, int* ptr) { return *ptr; } -Aggregate* FP_pointer_arithmetic_ok(Aggregate* a) { +Aggregate* pointer_arithmetic_ok(Aggregate* a) { a->~Aggregate(); a++; return a; diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index a213dd015..1fb54e9a5 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,13 +1,11 @@ -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(&(a))` at line 39, column 3 here,accessed `&(a)` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(&(a))` at line 53, column 3 here,accessed `&(a)` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(&(s))` at line 25, column 3 here,accessed `&(s)` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(a)` at line 77, column 3 here,accessed `a` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(&(a))` at line 100, column 3 here,accessed `&(a)` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(a)` at line 39, column 3 here,accessed `&(a.str)` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(a)` at line 53, column 3 here,accessed `&(a.a.str)` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(s)` at line 25, column 3 here,accessed `s.i` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(a)` at line 100, column 3 here,accessed `&(a)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] -codetoanalyze/cpp/pulse/returns.cpp, returns::return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `returns::S_~S(s)` at line 120, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `*(v.__internal_array)[_]` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 112, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 130, column 5 here,accessed `s` here] @@ -20,14 +18,14 @@ 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_basic_placement_new_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(tptr)` at line 118, column 3 here,accessed `ptr` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 162, column 3 here,accessed `&(s)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, 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_LIFETIME, 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, FP_destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 162, column 3 here,accessed `&(s)` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_placement_new_explicit_destructor_ok, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(*(s))` at line 43, column 5 here,accessed `&(buf)` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, 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_LIFETIME, 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, use_after_destructor_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `&(s)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 185, column 3 here,accessed `pc->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, 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_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 185, 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, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 56, column 5 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, FP_push_back_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 31, column 5 here,accessed `*(vec.__internal_array)[_]` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp index d9bcb4c5c..6df0fdbe9 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp @@ -113,9 +113,8 @@ int* return_deleted_bad() { return x; } -// this *could* be ok depending on what the destructor does, but there's -// probably no good reason to do it -S* return_destructed_pointer_bad() { +// this *could* be ok depending on what the caller does +S* return_destructed_pointer_ok() { S* s = new S(1); s->~S(); return s; diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 6ebc0f75f..0c974db3c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -36,7 +36,7 @@ int FP_reinit_after_explicit_destructor_ok() { return *s.f; } -void placement_new_explicit_destructor_ok() { +void FP_placement_new_explicit_destructor_ok() { char buf[sizeof(S)]; { S* s = new (buf) S(1); @@ -112,7 +112,7 @@ class Subclass : virtual POD { ~Subclass() { delete f; } }; -void FP_basic_placement_new_ok() { +void basic_placement_new_ok() { S* ptr = new S(1); S* tptr = new (ptr) S(1); tptr->~S();