[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

@@ -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 =

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]

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<std::string> v) {
-  int i = 0;
   for (int i = 0; i < 10; i++) {
     auto s = &v[i];
     delete s;