signature of show_trans* family of functions

The show_trans* family of functions now

1. gets the transition system as argument, as opposed to using ebmc_baset to create it;

2. gets the output stream as argument, as opposed to creating it itself.

Author: kroening

src/ebmc/ebmc_parse_options.cpp

@@ -202,17 +202,30 @@ int ebmc_parse_optionst::doit()
       // return do_two_phase_induction();
     }
 
+    // get the transition system
+    auto transition_system = get_transition_system(cmdline, ui_message_handler);
+
     if(cmdline.isset("show-trans"))
-      return show_trans(cmdline, ui_message_handler);
+    {
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet output_file{filename};
+      return show_trans(transition_system, output_file.stream());
+    }
 
     if(cmdline.isset("verilog-rtl"))
-      return show_trans_verilog_rtl(cmdline, ui_message_handler);
+    {
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet output_file{filename};
+      return show_trans_verilog_rtl(transition_system, output_file.stream());
+    }
 
     if(cmdline.isset("verilog-netlist"))
-      return show_trans_verilog_netlist(cmdline, ui_message_handler);
-
-    // get the transition system
-    auto transition_system = get_transition_system(cmdline, ui_message_handler);
+    {
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet output_file{filename};
+      return show_trans_verilog_netlist(
+        transition_system, output_file.stream());
+    }
 
     // get the properties
     auto properties = ebmc_propertiest::from_command_line(

src/ebmc/show_trans.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "show_trans.h"
 
+#include <util/cout_message.h>
+
 #include <verilog/expr2verilog.h>
 
 #include "ebmc_base.h"
@@ -25,23 +27,21 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-class show_transt:public ebmc_baset
+class show_transt
 {
 public:
-  show_transt(
-    const cmdlinet &cmdline,
-    ui_message_handlert &ui_message_handler):
-    ebmc_baset(cmdline, ui_message_handler)
+  explicit show_transt(const transition_systemt &_transition_system)
+    : transition_system(_transition_system)
   {
   }
 
-  int show_trans_verilog_rtl();
-  int show_trans_verilog_netlist();
-  int show_trans();
+  int show_trans_verilog_rtl(std::ostream &);
+  int show_trans_verilog_netlist(std::ostream &);
+  int show_trans(std::ostream &);
 
 protected:
-  int show_trans_verilog_rtl(std::ostream &out);
-  int show_trans_verilog_netlist(std::ostream &out);
+  const transition_systemt &transition_system;
+
   void verilog_header(std::ostream &out, const std::string &desc);
   void
   print_verilog_constraints(const exprt &, const namespacet &, std::ostream &);
@@ -60,11 +60,11 @@ Function: show_trans_verilog_netlist
 \*******************************************************************/
 
 int show_trans_verilog_netlist(
-  const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+  const transition_systemt &transition_system,
+  std::ostream &out)
 {
-  show_transt show_trans(cmdline, ui_message_handler);  
-  return show_trans.show_trans_verilog_netlist();
+  show_transt show_trans(transition_system);
+  return show_trans.show_trans_verilog_netlist(out);
 }
 
 /*******************************************************************\
@@ -80,11 +80,11 @@ Function: show_trans_verilog_rtl
 \*******************************************************************/
 
 int show_trans_verilog_rtl(
-  const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+  const transition_systemt &transition_system,
+  std::ostream &out)
 {
-  show_transt show_trans(cmdline, ui_message_handler);  
-  return show_trans.show_trans_verilog_rtl();
+  show_transt show_trans(transition_system);
+  return show_trans.show_trans_verilog_rtl(out);
 }
 
 /*******************************************************************\
@@ -101,8 +101,10 @@ Function: show_transt::show_trans_verilog_netlist
 
 int show_transt::show_trans_verilog_netlist(std::ostream &out)
 {
+  console_message_handlert message_handler;
+
   output_verilog_netlistt output_verilog(
-    transition_system.symbol_table, out, message.get_message_handler());
+    transition_system.symbol_table, out, message_handler);
 
   try
   {
@@ -145,8 +147,10 @@ Function: show_transt::show_trans_verilog_rtl
 
 int show_transt::show_trans_verilog_rtl(std::ostream &out)
 {
+  console_message_handlert message_handler;
+
   output_verilog_rtlt output_verilog(
-    transition_system.symbol_table, out, message.get_message_handler());
+    transition_system.symbol_table, out, message_handler);
 
   try
   {
@@ -177,6 +181,24 @@ int show_transt::show_trans_verilog_rtl(std::ostream &out)
 
 /*******************************************************************\
 
+Function: show_transt::show_trans
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int show_transt::show_trans(std::ostream &out)
+{
+  transition_system.output(out);
+  return 0;
+}
+
+/*******************************************************************\
+
 Function: show_transt::verilog_header
 
   Inputs:
@@ -226,86 +248,6 @@ void show_transt::print_verilog_constraints(
 
 /*******************************************************************\
 
-Function: show_transt::show_trans
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int show_transt::show_trans()
-{
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
-  transition_system.output(std::cout);
-
-  return 0;
-}
-
-/*******************************************************************\
-
-Function: show_transt::show_trans_verilog_rtl
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int show_transt::show_trans_verilog_rtl()
-{
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
-  if(cmdline.isset("outfile"))
-  {
-    const std::string filename=cmdline.get_value("outfile");
-    auto outfile = output_filet{filename};
-    show_trans_verilog_rtl(outfile.stream());
-  }
-  else
-    show_trans_verilog_rtl(std::cout);
-
-  return 0;
-}
-
-/*******************************************************************\
-
-Function: show_transt::show_trans_verilog_netlist
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int show_transt::show_trans_verilog_netlist()
-{
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
-  if(cmdline.isset("outfile"))
-  {
-    const std::string filename=cmdline.get_value("outfile");
-    auto outfile = output_filet{filename};
-    show_trans_verilog_netlist(outfile.stream());
-  }
-  else
-    show_trans_verilog_netlist(std::cout);
-
-  return 0;
-}
-
-/*******************************************************************\
-
 Function: show_trans
 
   Inputs:
@@ -316,11 +258,8 @@ Function: show_trans
 
 \*******************************************************************/
 
-int show_trans(
-  const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+int show_trans(const transition_systemt &transition_system, std::ostream &out)
 {
-  show_transt show_trans(cmdline, ui_message_handler);
-  return show_trans.show_trans();
+  show_transt show_trans(transition_system);
+  return show_trans.show_trans(out);
 }
-

src/ebmc/show_trans.h

@@ -9,12 +9,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_EBMC_SHOW_TRANS_H
 #define CPROVER_EBMC_SHOW_TRANS_H
 
-#include <util/cmdline.h>
-#include <util/ui_message.h>
+#include "transition_system.h"
 
-int show_trans_verilog_rtl(const cmdlinet &, ui_message_handlert &);
-int show_trans_verilog_netlist(const cmdlinet &, ui_message_handlert &);
-int show_trans_smv_netlist(const cmdlinet &, ui_message_handlert &);
-int show_trans(const cmdlinet &, ui_message_handlert &);
+int show_trans_verilog_rtl(const transition_systemt &, std::ostream &);
+int show_trans_verilog_netlist(const transition_systemt &, std::ostream &);
+int show_trans_smv_netlist(const transition_systemt &, std::ostream &);
+int show_trans(const transition_systemt &, std::ostream &);
 
-#endif
+#endif // CPROVER_EBMC_SHOW_TRANS_H