From f400d4c5c546d856c55f137ee7d8a3efa6940a09 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 5 Nov 2018 09:22:00 -0800 Subject: [PATCH] [pulse] always register havoc'd variables Summary: This prevents the join from wrongly assuming that we haven't seen a variable on one side of the join. Reviewed By: skcho Differential Revision: D12881987 fbshipit-source-id: 42a776adb --- infer/src/checkers/PulseDomain.ml | 4 +--- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp | 1 - 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index db7146ec1..6a4cb1bd1 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -547,9 +547,7 @@ module Operations = struct let havoc_var var astate = - if AliasingDomain.mem var astate.stack then - {astate with stack= AliasingDomain.remove var astate.stack} - else astate + {astate with stack= AliasingDomain.add var (AbstractAddress.mk_fresh ()) astate.stack} let havoc location (access_expr : AccessExpression.t) astate = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 97f83e3fa..d743d99ab 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -6,7 +6,7 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DE codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here] 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_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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp index 7967d3630..51d8a702c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp @@ -91,7 +91,6 @@ void delete_in_loop_ok() { } void delete_ref_in_loop_ok(int j, std::vector v) { - int i = 0; for (int i = 0; i < 10; i++) { auto s = &v[i]; delete s;