Preprocess shadow memory field declarations

Gathers the __CPROVER_field_decl* calls from
the goto model.

In the next step we'll pass them to goto_symex.

Author: peterschrammel

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
+#include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
@@ -72,6 +73,10 @@ operator()(propertiest &properties)
 
 void multi_path_symex_only_checkert::generate_equation()
 {
+  // Gather fields for shadow memory instrumentation
+  const auto fields =
+    shadow_memoryt::gather_field_declarations(goto_model, ui_message_handler);
+
   const auto symex_start = std::chrono::steady_clock::now();
 
   symex_symbol_table =

src/goto-checker/single_path_symex_only_checker.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/ui_message.h>
 
 #include <goto-symex/path_storage.h>
+#include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
@@ -73,6 +74,10 @@ void single_path_symex_only_checkert::initialize_worklist()
     unwindset);
   setup_symex(symex);
 
+  // Gather fields for shadow memory instrumentation
+  const auto fields =
+    shadow_memoryt::gather_field_declarations(goto_model, ui_message_handler);
+
   symex.initialize_path_storage_from_entry_point_of(
     goto_symext::get_goto_function(goto_model), symex_symbol_table);
 }