20
20
#include < langapi/mode.h>
21
21
22
22
#include " hw_cbmc_parse_options.h"
23
- #include " hw_bmc.h"
23
+ // #include "hw_bmc.h"
24
24
#include " map_vars.h"
25
25
#include " gen_interface.h"
26
26
@@ -50,7 +50,9 @@ int hw_cbmc_parse_optionst::doit()
50
50
51
51
optionst options;
52
52
get_command_line_options (options);
53
- eval_verbosity ();
53
+
54
+ eval_verbosity (
55
+ cmdline.get_value (" verbosity" ), messaget::M_STATISTICS, ui_message_handler);
54
56
55
57
//
56
58
// Print a banner
@@ -68,8 +70,10 @@ int hw_cbmc_parse_optionst::doit()
68
70
if (cmdline.isset (" vcd" ))
69
71
options.set_option (" vcd" , cmdline.get_value (" vcd" ));
70
72
73
+ symbol_tablet symbol_table;
74
+
71
75
cbmc_solverst cbmc_solvers (options, symbol_table, ui_message_handler);
72
- cbmc_solvers.set_ui (get_ui ());
76
+ cbmc_solvers.set_ui (ui_message_handler. get_ui ());
73
77
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
74
78
75
79
try
@@ -83,6 +87,7 @@ int hw_cbmc_parse_optionst::doit()
83
87
return 1 ;
84
88
}
85
89
90
+ #if 0
86
91
prop_convt &prop_conv=cbmc_solver->prop_conv();
87
92
hw_bmct hw_bmc(options, symbol_table, ui_message_handler, prop_conv);
88
93
@@ -110,6 +115,7 @@ int hw_cbmc_parse_optionst::doit()
110
115
111
116
// do actual BMC
112
117
return do_bmc(hw_bmc, goto_functions);
118
+ #endif
113
119
}
114
120
115
121
/* ******************************************************************\
@@ -172,7 +178,8 @@ Function: hw_cbmc_parse_optionst::get_modules
172
178
173
179
\*******************************************************************/
174
180
175
- int hw_cbmc_parse_optionst::get_modules (std::list<exprt> &bmc_constraints)
181
+ int hw_cbmc_parse_optionst::get_modules (
182
+ std::list<exprt> &bmc_constraints)
176
183
{
177
184
//
178
185
// unwinding of transition systems
@@ -229,7 +236,7 @@ int hw_cbmc_parse_optionst::get_modules(std::list<exprt> &bmc_constraints)
229
236
}
230
237
else if (cmdline.isset (" show-modules" ))
231
238
{
232
- show_modules (symbol_table, get_ui ());
239
+ show_modules (symbol_table, ui_message_handler. get_ui ());
233
240
return 0 ; // done
234
241
}
235
242
0 commit comments