Skip to content

Commit

Permalink
Merge pull request #877 from diffblue/use-output-filet
Browse files Browse the repository at this point in the history
ebmc: --smt-netlist and --dot-netlist now honor --outfile
  • Loading branch information
tautschnig authored Dec 6, 2024
2 parents 7c7e7e2 + a6d7be0 commit a7e28cd
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 8 deletions.
1 change: 1 addition & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
* SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
* SystemVerilog: set membership operator
* SystemVerilog: named sequences
* ebmc: --smt-netlist and --dot-netlist now honor --outfile

# EBMC 5.3

Expand Down
24 changes: 16 additions & 8 deletions src/ebmc/ebmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
#include "ic3_engine.h"
#include "liveness_to_safety.h"
#include "neural_liveness.h"
#include "output_file.h"
#include "property_checker.h"
#include "random_traces.h"
#include "ranking_function.h"
Expand Down Expand Up @@ -274,9 +275,12 @@ int ebmc_parse_optionst::doit()
netlistt netlist;
if(ebmc_base.make_netlist(netlist))
return 1;
std::cout << "digraph netlist {\n";
netlist.output_dot(std::cout);
std::cout << "}\n";
auto filename =
cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
output_filet outfile{filename};
outfile.stream() << "digraph netlist {\n";
netlist.output_dot(outfile.stream());
outfile.stream() << "}\n";
return 0;
}

Expand All @@ -285,11 +289,15 @@ int ebmc_parse_optionst::doit()
netlistt netlist;
if(ebmc_base.make_netlist(netlist))
return 1;
std::cout << "-- Generated by EBMC " << EBMC_VERSION << '\n';
std::cout << "-- Generated from "
<< ebmc_base.transition_system.main_symbol->name << '\n';
std::cout << '\n';
netlist.output_smv(std::cout);
auto filename =
cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
output_filet outfile{filename};
outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
outfile.stream() << "-- Generated from "
<< ebmc_base.transition_system.main_symbol->name
<< '\n';
outfile.stream() << '\n';
netlist.output_smv(outfile.stream());
return 0;
}

Expand Down

0 comments on commit a7e28cd

Please sign in to comment.