Bugfix: Maintain safe_pointers per-path

regression/cbmc/path-branch-pointer-call/main.c

@@ -0,0 +1,17 @@
+int foo(int *x)
+{
+  if(*x)
+  {
+    int y = 9;
+  }
+  else
+  {
+    int z = 4;
+  }
+}
+
+int main()
+{
+  int x;
+  foo(&x);
+}

regression/cbmc/path-branch-pointer-call/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/goto_symex.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 
-#include <analyses/local_safe_pointers.h>
-
 #include <util/options.h>
 #include <util/message.h>
 
@@ -468,8 +466,6 @@ class goto_symext
   void rewrite_quantifiers(exprt &, statet &);
 
   path_storaget &path_storage;
-
-  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/goto_symex_state.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <analyses/dirty.h>
+#include <analyses/local_safe_pointers.h>
 
 #include <util/invariant.h>
 #include <util/guard.h>
@@ -197,6 +198,8 @@ class goto_symex_statet final
   l1_typest l1_types;
 
 public:
+  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
+
   // uses level 1 names, and is used to
   // do dereferencing
   value_sett value_set;
@@ -211,6 +214,7 @@ class goto_symex_statet final
     symex_targett::sourcet source;
     propagationt propagation;
     unsigned atomic_section_id;
+    std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
     explicit goto_statet(const goto_symex_statet &s):
       depth(s.depth),
@@ -219,7 +223,8 @@ class goto_symex_statet final
       guard(s.guard),
       source(s.source),
       propagation(s.propagation),
-      atomic_section_id(s.atomic_section_id)
+      atomic_section_id(s.atomic_section_id),
+      safe_pointers(s.safe_pointers)
     {
     }
 
@@ -247,6 +252,7 @@ class goto_symex_statet final
       guard(s.guard),
       source(s.source),
       propagation(s.propagation),
+      safe_pointers(s.safe_pointers),
       value_set(s.value_set),
       atomic_section_id(s.atomic_section_id)
   {

src/goto-symex/symex_dereference.cpp

@@ -247,7 +247,7 @@ void goto_symext::dereference_rec(
         state.get_original_name(to_check);
 
         expr_is_not_null =
-          safe_pointers.at(expr_function).is_safe_dereference(
+          state.safe_pointers.at(expr_function).is_safe_dereference(
             to_check, state.source.pc);
       }
     }

src/goto-symex/symex_function_call.cpp

@@ -225,7 +225,7 @@ void goto_symext::symex_function_call_code(
   state.dirty.populate_dirty_for_function(identifier, goto_function);
 
   auto emplace_safe_pointers_result =
-    safe_pointers.emplace(identifier, local_safe_pointerst{ns});
+    state.safe_pointers.emplace(identifier, local_safe_pointerst{ns});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(goto_function.body);
 

src/goto-symex/symex_main.cpp

@@ -136,7 +136,7 @@ void goto_symext::initialize_entry_point(
   const goto_functiont &entry_point_function = get_goto_function(pc->function);
 
   auto emplace_safe_pointers_result =
-    safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
+    state.safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(entry_point_function.body);