Move goto_statet definition to its own file

Having one class per header file makes it easier to navigate the code
and find what we want.

Author: romainbrenguier

src/goto-symex/Makefile

@@ -1,5 +1,6 @@
 SRC = auto_objects.cpp \
       build_goto_trace.cpp \
+      goto_state.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \
       memory_model.cpp \

src/goto-symex/goto_state.cpp

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include "goto_state.h"
+
+#include <util/format_expr.h>
+
+/// Print the constant propagation map in a human-friendly format.
+/// This is primarily for use from the debugger; please don't delete me just
+/// because there aren't any current callers.
+void goto_statet::output_propagation_map(std::ostream &out)
+{
+  for(const auto &name_value : propagation)
+  {
+    out << name_value.first << " <- " << format(name_value.second) << "\n";
+  }
+}

src/goto-symex/goto_state.h

@@ -0,0 +1,71 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// goto_statet class definition
+
+#ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
+#define CPROVER_GOTO_SYMEX_GOTO_STATE_H
+
+#include <analyses/local_safe_pointers.h>
+#include <pointer-analysis/value_set.h>
+#include <util/guard.h>
+
+#include "renaming_level.h"
+#include "symex_target_equation.h"
+
+/// Container for data that varies per program point, e.g. the constant
+/// propagator state, when state needs to branch. This is copied out of
+/// goto_symex_statet at a control-flow fork and then back into it at a
+/// control-flow merge.
+class goto_statet
+{
+public:
+  /// Distance from entry
+  unsigned depth = 0;
+
+  symex_level2t level2;
+
+  /// Uses level 1 names, and is used to do dereferencing
+  value_sett value_set;
+
+  // A guard is a particular condition that has to pass for an instruction
+  // to be executed. The easiest example is an if/else: each instruction along
+  // the if branch will be guarded by the condition of the if (and if there
+  // is an else branch then instructions on it will be guarded by the negation
+  // of the condition of the if).
+  guardt guard{true_exprt{}};
+
+  symex_targett::sourcet source;
+
+  // Map L1 names to (L2) constants. Values will be evicted from this map
+  // when they become non-constant. This is used to propagate values that have
+  // been worked out to only have one possible value.
+  //
+  // "constants" can include symbols, but only in the context of an address-of
+  // op (i.e. &x can be propagated), and an address-taken thing should only be
+  // L1.
+  std::map<irep_idt, exprt> propagation;
+
+  void output_propagation_map(std::ostream &);
+
+  /// Threads
+  unsigned atomic_section_id = 0;
+
+  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
+  unsigned total_vccs = 0;
+  unsigned remaining_vccs = 0;
+
+  /// Constructors
+  explicit goto_statet(const class goto_symex_statet &s);
+  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
+  {
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/goto_symex_state.cpp

@@ -785,14 +785,3 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
         << frame.calling_location.pc->location_number << "\n";
   }
 }
-
-/// Print the constant propagation map in a human-friendly format.
-/// This is primarily for use from the debugger; please don't delete me just
-/// because there aren't any current callers.
-void goto_statet::output_propagation_map(std::ostream &out)
-{
-  for(const auto &name_value : propagation)
-  {
-    out << name_value.first << " <- " << format(name_value.second) << "\n";
-  }
-}

src/goto-symex/goto_symex_state.h

@@ -16,69 +16,18 @@ 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>
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
 #include <util/make_unique.h>
-
-#include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_function.h>
 
+#include "goto_state.h"
 #include "renaming_level.h"
 #include "symex_target_equation.h"
 
-/// Container for data that varies per program point, e.g. the constant
-/// propagator state, when state needs to branch. This is copied out of
-/// goto_symex_statet at a control-flow fork and then back into it at a
-/// control-flow merge.
-class goto_statet
-{
-public:
-  /// Distance from entry
-  unsigned depth = 0;
-
-  symex_level2t level2;
-
-  /// Uses level 1 names, and is used to do dereferencing
-  value_sett value_set;
-
-  // A guard is a particular condition that has to pass for an instruction
-  // to be executed. The easiest example is an if/else: each instruction along
-  // the if branch will be guarded by the condition of the if (and if there
-  // is an else branch then instructions on it will be guarded by the negation
-  // of the condition of the if).
-  guardt guard{true_exprt{}};
-
-  symex_targett::sourcet source;
-
-  // Map L1 names to (L2) constants. Values will be evicted from this map
-  // when they become non-constant. This is used to propagate values that have
-  // been worked out to only have one possible value.
-  //
-  // "constants" can include symbols, but only in the context of an address-of
-  // op (i.e. &x can be propagated), and an address-taken thing should only be
-  // L1.
-  std::map<irep_idt, exprt> propagation;
-
-  void output_propagation_map(std::ostream &);
-
-  /// Threads
-  unsigned atomic_section_id = 0;
-
-  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
-  unsigned total_vccs = 0;
-  unsigned remaining_vccs = 0;
-
-  /// Constructors
-  explicit goto_statet(const class goto_symex_statet &s);
-  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
-  {
-  }
-};
-
 // stack frames -- these are used for function calls and
 // for exceptions
 struct framet