diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 573c43932..415fb9037 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -202,15 +202,6 @@ int ebmc_parse_optionst::doit() // return do_two_phase_induction(); } - if(cmdline.isset("show-trans")) - return show_trans(cmdline, ui_message_handler); - - if(cmdline.isset("verilog-rtl")) - return show_trans_verilog_rtl(cmdline, ui_message_handler); - - 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); @@ -218,15 +209,6 @@ int ebmc_parse_optionst::doit() auto properties = ebmc_propertiest::from_command_line( cmdline, transition_system, ui_message_handler); - if(cmdline.isset("smv-word-level")) - { - auto filename = cmdline.value_opt("outfile").value_or("-"); - output_filet output_file{filename}; - output_smv_word_level( - transition_system, properties, output_file.stream()); - return 0; - } - if(cmdline.isset("show-properties")) { show_properties(properties, ui_message_handler); @@ -243,6 +225,37 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("liveness-to-safety")) liveness_to_safety(transition_system, properties); + if(cmdline.isset("smv-word-level")) + { + auto filename = cmdline.value_opt("outfile").value_or("-"); + output_filet output_file{filename}; + output_smv_word_level( + transition_system, properties, output_file.stream()); + return 0; + } + + if(cmdline.isset("show-trans")) + { + 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")) + { + 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")) + { + auto filename = cmdline.value_opt("outfile").value_or("-"); + output_filet output_file{filename}; + return show_trans_verilog_netlist( + transition_system, output_file.stream()); + } + if(cmdline.isset("show-varmap")) { auto netlist = diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp index 0c1a2bbc3..3e2c0aa94 100644 --- a/src/ebmc/show_trans.cpp +++ b/src/ebmc/show_trans.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "show_trans.h" +#include + #include #include "ebmc_base.h" @@ -25,23 +27,21 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -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); } - diff --git a/src/ebmc/show_trans.h b/src/ebmc/show_trans.h index bbc2bbd55..3f50f56b3 100644 --- a/src/ebmc/show_trans.h +++ b/src/ebmc/show_trans.h @@ -9,12 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_EBMC_SHOW_TRANS_H #define CPROVER_EBMC_SHOW_TRANS_H -#include -#include +#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