Bugfix: Maintain safe_pointers per-path

The map of safe pointers is now maintained separately for each path,
ensuring that pointer accesses on one path do not influence a (lack of)
pointer accesses on a different path.

This commit fixes diffblue#2866, a segfault that would happen when running CBMC
on the included regression test.

Author: karkhaz

regression/cbmc-path/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>" -X smt-backend
+)

regression/cbmc-path/Makefile

@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log

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