Merge pull request diffblue#2175 from diffblue/extract-goto-functiont

split out goto_functiont from goto_functions.h into separate file

Author: Daniel Kroening

src/analyses/local_cfg.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/numbering.h>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_program.h>
 
 class local_cfgt
 {

src/analyses/locals.h

@@ -14,13 +14,11 @@ Date: March 2013
 #ifndef CPROVER_ANALYSES_LOCALS_H
 #define CPROVER_ANALYSES_LOCALS_H
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_function.h>
 
 class localst
 {
 public:
-  typedef goto_functionst::goto_functiont goto_functiont;
-
   explicit localst(const goto_functiont &goto_function)
   {
     build(goto_function);

src/goto-instrument/alignment_checks.cpp

@@ -12,7 +12,11 @@ Module: Alignment Checks
 #include "alignment_checks.h"
 
 #include <util/config.h>
+#include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_types.h>
+
+#include <ostream>
 
 void print_struct_alignment_problems(
   const symbol_tablet &symbol_table,

src/goto-instrument/alignment_checks.h

@@ -14,7 +14,7 @@ Module: Alignment Checks
 
 #include <iosfwd>
 
-#include <goto-programs/goto_functions.h>
+#include <util/symbol_table.h>
 
 void print_struct_alignment_problems(
   const symbol_tablet &symbol_table,

src/goto-programs/Makefile

@@ -15,6 +15,7 @@ SRC = basic_blocks.cpp \
       goto_convert_function_call.cpp \
       goto_convert_functions.cpp \
       goto_convert_side_effect.cpp \
+      goto_function.cpp \
       goto_functions.cpp \
       goto_inline.cpp \
       goto_inline_class.cpp \

src/goto-programs/generate_function_bodies.h

@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
 #include <memory>
 #include <regex>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
 #include <util/cmdline.h>
 #include <util/message.h>

src/goto-programs/goto_function.cpp

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: A GOTO Function
+
+Author: Daniel Kroening
+
+Date: May 2018
+
+\*******************************************************************/
+
+#include "goto_function.h"
+
+void get_local_identifiers(
+  const goto_functiont &goto_function,
+  std::set<irep_idt> &dest)
+{
+  goto_function.body.get_decl_identifiers(dest);
+
+  const code_typet::parameterst &parameters = goto_function.type.parameters();
+
+  // add parameters
+  for(const auto &param : parameters)
+  {
+    const irep_idt &identifier = param.get_identifier();
+    if(identifier != "")
+      dest.insert(identifier);
+  }
+}

src/goto-programs/goto_function.h

@@ -0,0 +1,103 @@
+/*******************************************************************\
+
+Module: A GOTO Function
+
+Author: Daniel Kroening
+
+Date: May 2018
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
+#define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
+
+#include <iosfwd>
+
+#include <util/std_types.h>
+
+#include "goto_program.h"
+
+class goto_functiont
+{
+public:
+  goto_programt body;
+  code_typet type;
+
+  typedef std::vector<irep_idt> parameter_identifierst;
+  parameter_identifierst parameter_identifiers;
+
+  bool body_available() const
+  {
+    return !body.instructions.empty();
+  }
+
+  bool is_inlined() const
+  {
+    return type.get_bool(ID_C_inlined);
+  }
+
+  bool is_hidden() const
+  {
+    return type.get_bool(ID_C_hide);
+  }
+
+  void make_hidden()
+  {
+    type.set(ID_C_hide, true);
+  }
+
+  goto_functiont()
+  {
+  }
+
+  void clear()
+  {
+    body.clear();
+    type.clear();
+    parameter_identifiers.clear();
+  }
+
+  /// update the function member in each instruction
+  /// \param function_id: the `function_id` used for assigning empty function
+  ///   members
+  void update_instructions_function(const irep_idt &function_id)
+  {
+    body.update_instructions_function(function_id);
+  }
+
+  void swap(goto_functiont &other)
+  {
+    body.swap(other.body);
+    type.swap(other.type);
+    parameter_identifiers.swap(other.parameter_identifiers);
+  }
+
+  void copy_from(const goto_functiont &other)
+  {
+    body.copy_from(other.body);
+    type = other.type;
+    parameter_identifiers = other.parameter_identifiers;
+  }
+
+  goto_functiont(const goto_functiont &) = delete;
+  goto_functiont &operator=(const goto_functiont &) = delete;
+
+  goto_functiont(goto_functiont &&other)
+    : body(std::move(other.body)),
+      type(std::move(other.type)),
+      parameter_identifiers(std::move(other.parameter_identifiers))
+  {
+  }
+
+  goto_functiont &operator=(goto_functiont &&other)
+  {
+    body = std::move(other.body);
+    type = std::move(other.type);
+    parameter_identifiers = std::move(other.parameter_identifiers);
+    return *this;
+  }
+};
+
+void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
+
+#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H

src/goto-programs/goto_functions.cpp

@@ -73,22 +73,3 @@ void goto_functionst::compute_loop_numbers()
     func.second.body.compute_loop_numbers();
   }
 }
-
-
-void get_local_identifiers(
-  const goto_functiont &goto_function,
-  std::set<irep_idt> &dest)
-{
-  goto_function.body.get_decl_identifiers(dest);
-
-  const code_typet::parameterst &parameters=
-    goto_function.type.parameters();
-
-  // add parameters
-  for(const auto &param : parameters)
-  {
-    const irep_idt &identifier=param.get_identifier();
-    if(identifier!="")
-      dest.insert(identifier);
-  }
-}

src/goto-programs/goto_functions.h

@@ -14,93 +14,9 @@ Date: June 2003
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
 
-#include <iosfwd>
+#include "goto_function.h"
 
 #include <util/cprover_prefix.h>
-#include <util/std_types.h>
-
-#include "goto_program.h"
-
-class goto_functiont
-{
-public:
-  goto_programt body;
-  code_typet type;
-
-  typedef std::vector<irep_idt> parameter_identifierst;
-  parameter_identifierst parameter_identifiers;
-
-  bool body_available() const
-  {
-    return !body.instructions.empty();
-  }
-
-  bool is_inlined() const
-  {
-    return type.get_bool(ID_C_inlined);
-  }
-
-  bool is_hidden() const
-  {
-    return type.get_bool(ID_C_hide);
-  }
-
-  void make_hidden()
-  {
-    type.set(ID_C_hide, true);
-  }
-
-  goto_functiont()
-  {
-  }
-
-  void clear()
-  {
-    body.clear();
-    type.clear();
-    parameter_identifiers.clear();
-  }
-
-  /// update the function member in each instruction
-  /// \param function_id: the `function_id` used for assigning empty function
-  ///   members
-  void update_instructions_function(const irep_idt &function_id)
-  {
-    body.update_instructions_function(function_id);
-  }
-
-  void swap(goto_functiont &other)
-  {
-    body.swap(other.body);
-    type.swap(other.type);
-    parameter_identifiers.swap(other.parameter_identifiers);
-  }
-
-  void copy_from(const goto_functiont &other)
-  {
-    body.copy_from(other.body);
-    type=other.type;
-    parameter_identifiers=other.parameter_identifiers;
-  }
-
-  goto_functiont(const goto_functiont &)=delete;
-  goto_functiont &operator=(const goto_functiont &)=delete;
-
-  goto_functiont(goto_functiont &&other):
-    body(std::move(other.body)),
-    type(std::move(other.type)),
-    parameter_identifiers(std::move(other.parameter_identifiers))
-  {
-  }
-
-  goto_functiont &operator=(goto_functiont &&other)
-  {
-    body=std::move(other.body);
-    type=std::move(other.type);
-    parameter_identifiers=std::move(other.parameter_identifiers);
-    return *this;
-  }
-};
 
 class goto_functionst
 {
@@ -211,8 +127,4 @@ class goto_functionst
       it=(functions).function_map.begin(); \
       it!=(functions).function_map.end(); it++)
 
-void get_local_identifiers(
-  const goto_functiont &,
-  std::set<irep_idt> &dest);
-
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H

src/goto-symex/goto_symex_state.h

@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/make_unique.h>
 
 #include <pointer-analysis/value_set.h>
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_function.h>
 
 #include "symex_target_equation.h"
 
@@ -365,7 +365,7 @@ class goto_symex_statet final
   bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
 
   void populate_dirty_for_function(
-    const irep_idt &id, const goto_functionst::goto_functiont &);
+    const irep_idt &id, const goto_functiont &);
 
   void switch_to_thread(unsigned t);
   bool record_events;