Skip to content

signature of show_trans* family of functions #1125

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 28, 2025
+82 −131
Merged

signature of show_trans* family of functions #1125

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 31 additions & 18 deletions src/ebmc/ebmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,31 +202,13 @@ 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);

// get the properties
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);
Expand All @@ -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 =
Expand Down
151 changes: 45 additions & 106 deletions src/ebmc/show_trans.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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 &);
Expand All @@ -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);
}

/*******************************************************************\
Expand All @@ -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);
}

/*******************************************************************\
Expand All @@ -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
{
Expand Down Expand Up @@ -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
{
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand All @@ -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);
}

13 changes: 6 additions & 7 deletions src/ebmc/show_trans.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading