Bugfix: Maintain safe_pointers per-path

[karkhaz]

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 #2866, a segfault that would happen when running CBMC
on the included regression test.

[tautschnig]

Please add this directory to regression/Makefile and regression/CMakeLists.txt -- although I'm not sure a new directory is strictly required, it might be safe to include that test in the cbmc/ folder?

[karkhaz]

@tautschnig thanks, I moved the test over to regression/cbmc/

[smowton]

Sorry this comment is late, just getting back from holiday. This doesn't make sense to me currently, as the safe-pointers analysis isn't path sensitive-- this is a very local analysis looking for accesses trivially dominated by checks. The result should therefore always be the same, hence keeping them globally. It should have the same usage pattern as dirtyt in this respect. So what's going on here?

[karkhaz]

I'm actually not sure about this. As far as I can see, values are only added to that map in two places in the codebase (symex_dereference.cpp:250 and symex_function_call.cpp:228), and the keys shouldn't be going out of scope or being mysteriously removed or anything. Let's wait for @tautschnig to get back from holiday, he suggested the fix?

However, note that dirtyt is also owned by goto_symex_statet. IIRC, I moved it there for exactly the same reason when I wrote the original path exploration code (it's been a while now, can't remember what the exact problems were, but that's why the class now has the awkward copy constructor).