Skip to content

Commit cf5b15c

Browse files
committed
move --show-ldg out of ebmc_baset
1 parent 56bf074 commit cf5b15c

File tree

3 files changed

+14
-37
lines changed

3 files changed

+14
-37
lines changed

src/ebmc/ebmc_base.cpp

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -61,38 +61,6 @@ int ebmc_baset::get_properties()
6161

6262
/*******************************************************************\
6363
64-
Function: ebmc_baset::show_ldg
65-
66-
Inputs:
67-
68-
Outputs:
69-
70-
Purpose:
71-
72-
\*******************************************************************/
73-
74-
void ebmc_baset::show_ldg(std::ostream &out)
75-
{
76-
netlistt netlist;
77-
78-
if(make_netlist(netlist))
79-
return;
80-
81-
if(!netlist.transition.empty())
82-
out << "WARNING: transition constraint found!" << '\n'
83-
<< '\n';
84-
85-
ldgt ldg;
86-
87-
ldg.compute(netlist);
88-
89-
out << "Latch dependencies:" << '\n';
90-
91-
ldg.output(netlist, out);
92-
}
93-
94-
/*******************************************************************\
95-
9664
Function: ebmc_baset::make_netlist
9765
9866
Inputs:

src/ebmc/ebmc_base.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ class ebmc_baset
3333
virtual ~ebmc_baset() { }
3434

3535
int get_properties();
36-
void show_ldg(std::ostream &out);
3736
bool make_netlist(netlistt &);
3837

3938
transition_systemt transition_system;

src/ebmc/ebmc_parse_options.cpp

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#include <util/help_formatter.h>
1414
#include <util/string2int.h>
1515

16+
#include <trans-netlist/ldg.h>
1617
#include <trans-netlist/smv_netlist.h>
1718

1819
#include "build_transition_system.h"
@@ -270,10 +271,19 @@ int ebmc_parse_optionst::doit()
270271

271272
if(cmdline.isset("show-ldg"))
272273
{
273-
ebmc_baset ebmc_base(cmdline, ui_message_handler);
274-
ebmc_base.transition_system = std::move(transition_system);
275-
ebmc_base.properties = std::move(properties);
276-
ebmc_base.show_ldg(std::cout);
274+
auto netlist =
275+
make_netlist(transition_system, properties, ui_message_handler);
276+
277+
if(!netlist.transition.empty())
278+
{
279+
messaget message(ui_message_handler);
280+
message.warning() << "transition constraint found!" << messaget::eom;
281+
}
282+
283+
ldgt ldg;
284+
ldg.compute(netlist);
285+
std::cout << "Latch dependencies:" << '\n';
286+
ldg.output(netlist, std::cout);
277287
return 0;
278288
}
279289

0 commit comments

Comments
 (0)