further goto_modelt APIs

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3867 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-programs/goto_convert_functions.cpp

@@ -289,6 +289,27 @@ Function: goto_convert
 
 \*******************************************************************/
 
+void goto_convert(
+  symbol_tablet &symbol_table,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  goto_convert(symbol_table, goto_model.goto_functions, message_handler);
+  goto_model.symbol_table.swap(symbol_table);
+}
+
+/*******************************************************************\
+
+Function: goto_convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void goto_convert(
   symbol_tablet &symbol_table,
   goto_functionst &functions,

src/goto-programs/goto_convert_functions.h

@@ -11,7 +11,7 @@ Date: June 2003
 #ifndef CPROVER_GOTO_CONVERT_FUNCTIONS_H
 #define CPROVER_GOTO_CONVERT_FUNCTIONS_H
 
-#include "goto_functions.h"
+#include "goto_model.h"
 #include "goto_convert_class.h"
 
 // convert it all!
@@ -20,6 +20,12 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &message_handler);
 
+// convert it all!
+void goto_convert(
+  symbol_tablet &symbol_table,
+  goto_modelt &dest,
+  message_handlert &message_handler);
+  
 // just convert a specific function
 void goto_convert(
   const irep_idt &identifier,

src/goto-programs/link_to_library.cpp

@@ -24,6 +24,28 @@ Function: link_to_library
 
 \*******************************************************************/
 
+void link_to_library(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  link_to_library(
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    message_handler);
+}
+
+/*******************************************************************\
+
+Function: link_to_library
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void link_to_library(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions,

src/goto-programs/link_to_library.h

@@ -11,11 +11,15 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 
-#include "goto_functions.h"
+#include "goto_model.h"
 
 void link_to_library(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions,
-  message_handlert &message_handler);
+  symbol_tablet &,
+  goto_functionst &,
+  message_handlert &);
+
+void link_to_library(
+  goto_modelt &,
+  message_handlert &);
 
 #endif

src/goto-programs/loop_ids.cpp

@@ -26,6 +26,25 @@ Function: show_loop_ids
 
 \*******************************************************************/
 
+void show_loop_ids(
+  ui_message_handlert::uit ui,
+  const goto_modelt &goto_model)
+{
+  show_loop_ids(ui, goto_model.goto_functions);
+}
+
+/*******************************************************************\
+
+Function: show_loop_ids
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void show_loop_ids(
   ui_message_handlert::uit ui,
   const goto_programt &goto_program)

src/goto-programs/loop_ids.h

@@ -11,14 +11,18 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 
-#include "goto_functions.h"
+#include "goto_model.h"
 
 void show_loop_ids(
-  ui_message_handlert::uit ui,
-  const goto_functionst &goto_functions);
+  ui_message_handlert::uit,
+  const goto_modelt &);
 
 void show_loop_ids(
-  ui_message_handlert::uit ui,
-  const goto_programt &goto_program);
+  ui_message_handlert::uit,
+  const goto_functionst &);
+
+void show_loop_ids(
+  ui_message_handlert::uit,
+  const goto_programt &);
 
 #endif

src/goto-programs/set_properties.cpp

@@ -58,6 +58,23 @@ Function: label_properties
 
 \*******************************************************************/
 
+void label_properties(goto_modelt &goto_model)
+{
+  label_properties(goto_model.goto_functions);
+}
+
+/*******************************************************************\
+
+Function: label_properties
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void label_properties(
   goto_programt &goto_program,
   std::map<irep_idt, unsigned> &property_counters)
@@ -112,6 +129,25 @@ Function: set_properties
 
 \*******************************************************************/
 
+void set_properties(
+  goto_modelt &goto_model,
+  const std::list<std::string> &properties)
+{
+  set_properties(goto_model.goto_functions, properties);
+}
+
+/*******************************************************************\
+
+Function: set_properties
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void set_properties(
   goto_functionst &goto_functions,
   const std::list<std::string> &properties)
@@ -171,6 +207,23 @@ Function: make_assertions_false
 
 \*******************************************************************/
 
+void make_assertions_false(goto_modelt &goto_model)
+{
+  make_assertions_false(goto_model.goto_functions);
+}
+
+/*******************************************************************\
+
+Function: make_assertions_false
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void make_assertions_false(
   goto_functionst &goto_functions)
 {

src/goto-programs/set_properties.h

@@ -9,15 +9,21 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
 #define CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
 
-#include <goto-programs/goto_functions.h>
+#include "goto_model.h"
 
 void set_properties(
   goto_functionst &goto_functions,
   const std::list<std::string> &properties);
 
+void set_properties(
+  goto_modelt &goto_model,
+  const std::list<std::string> &properties);
+
 void make_assertions_false(goto_functionst &);  
+void make_assertions_false(goto_modelt &);  
 
 void label_properties(goto_functionst &);
 void label_properties(goto_programt &);
+void label_properties(goto_modelt &);
 
 #endif