Skip to content

Commit f93fb2c

Browse files
author
Daniel Kroening
committed
use formatter in show_symbol_table
1 parent 1e7fb0a commit f93fb2c

File tree

5 files changed

+59
-60
lines changed

5 files changed

+59
-60
lines changed

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include <langapi/language.h>
2626

2727
#include <ansi-c/c_preprocess.h>
28+
#include <ansi-c/ansi_c_formatter.h>
2829

2930
#include <goto-programs/adjust_float_expressions.h>
3031
#include <goto-programs/initialize_goto_model.h>
@@ -595,7 +596,9 @@ int cbmc_parse_optionst::get_goto_program(
595596

596597
if(cmdline.isset("show-symbol-table"))
597598
{
598-
show_symbol_table(goto_model, ui_message_handler.get_ui());
599+
namespacet ns(goto_model.symbol_table);
600+
ansi_c_formattert formatter(ns);
601+
show_symbol_table(goto_model, ui_message_handler.get_ui(), formatter);
599602
return CPROVER_EXIT_SUCCESS;
600603
}
601604

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
2121
#include <util/json.h>
2222
#include <util/exit_codes.h>
2323

24+
#include <ansi-c/ansi_c_formatter.h>
25+
2426
#include <goto-programs/class_hierarchy.h>
2527
#include <goto-programs/goto_convert_functions.h>
2628
#include <goto-programs/remove_calls_no_body.h>
@@ -463,7 +465,9 @@ int goto_instrument_parse_optionst::doit()
463465

464466
if(cmdline.isset("show-symbol-table"))
465467
{
466-
::show_symbol_table(goto_model, get_ui());
468+
namespacet ns(goto_model.symbol_table);
469+
ansi_c_formattert formatter(ns);
470+
::show_symbol_table(goto_model, get_ui(), formatter);
467471
return CPROVER_EXIT_SUCCESS;
468472
}
469473

‎src/goto-programs/show_symbol_table.cpp

Lines changed: 34 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,14 @@ Author: Daniel Kroening, [email protected]
1919

2020
#include "goto_model.h"
2121

22-
void show_symbol_table_xml_ui()
22+
void show_symbol_table_xml_ui(formattert &)
2323
{
2424
}
2525

2626
void show_symbol_table_brief_plain(
2727
const symbol_tablet &symbol_table,
28-
std::ostream &out)
28+
std::ostream &out,
29+
formattert &formatter)
2930
{
3031
// we want to sort alphabetically
3132
std::set<std::string> symbols;
@@ -41,29 +42,17 @@ void show_symbol_table_brief_plain(
4142
{
4243
const symbolt &symbol=ns.lookup(id);
4344

44-
std::unique_ptr<languaget> ptr;
45-
46-
if(symbol.mode=="")
47-
ptr=get_default_language();
48-
else
49-
{
50-
ptr=get_language_from_mode(symbol.mode);
51-
if(ptr==nullptr)
52-
throw "symbol "+id2string(symbol.name)+" has unknown mode";
53-
}
54-
55-
std::string type_str;
56-
5745
if(symbol.type.is_not_nil())
58-
ptr->from_type(symbol.type, type_str, ns);
59-
60-
out << symbol.name << " " << type_str << '\n';
46+
out << symbol.name << " " << formatter(symbol.type) << '\n';
47+
else
48+
out << symbol.name << '\n';
6149
}
6250
}
6351

6452
void show_symbol_table_plain(
6553
const symbol_tablet &symbol_table,
66-
std::ostream &out)
54+
std::ostream &out,
55+
formattert &formatter)
6756
{
6857
out << '\n' << "Symbols:" << '\n' << '\n';
6958

@@ -81,35 +70,24 @@ void show_symbol_table_plain(
8170
{
8271
const symbolt &symbol=ns.lookup(id);
8372

84-
std::unique_ptr<languaget> ptr;
85-
86-
if(symbol.mode=="")
87-
{
88-
ptr=get_default_language();
89-
}
90-
else
91-
{
92-
ptr=get_language_from_mode(symbol.mode);
93-
}
94-
95-
if(!ptr)
96-
throw "symbol "+id2string(symbol.name)+" has unknown mode";
97-
9873
std::string type_str, value_str;
9974

100-
if(symbol.type.is_not_nil())
101-
ptr->from_type(symbol.type, type_str, ns);
102-
103-
if(symbol.value.is_not_nil())
104-
ptr->from_expr(symbol.value, value_str, ns);
105-
10675
out << "Symbol......: " << symbol.name << '\n' << std::flush;
10776
out << "Pretty name.: " << symbol.pretty_name << '\n';
10877
out << "Module......: " << symbol.module << '\n';
10978
out << "Base name...: " << symbol.base_name << '\n';
11079
out << "Mode........: " << symbol.mode << '\n';
111-
out << "Type........: " << type_str << '\n';
112-
out << "Value.......: " << value_str << '\n';
80+
81+
out << "Type........: ";
82+
if(symbol.type.is_not_nil())
83+
out << formatter(symbol.type);
84+
out << '\n';
85+
86+
out << "Value.......: ";
87+
if(symbol.value.is_not_nil())
88+
out << formatter(symbol.value);
89+
out << '\n';
90+
11391
out << "Flags.......:";
11492

11593
if(symbol.is_lvalue)
@@ -146,24 +124,25 @@ void show_symbol_table_plain(
146124
out << " volatile";
147125

148126
out << '\n';
149-
out << "Location....: " << symbol.location << '\n';
127+
out << "Location....: " << formatter(symbol.location) << '\n';
150128

151129
out << '\n' << std::flush;
152130
}
153131
}
154132

155133
void show_symbol_table(
156134
const symbol_tablet &symbol_table,
157-
ui_message_handlert::uit ui)
135+
ui_message_handlert::uit ui,
136+
formattert &formatter)
158137
{
159138
switch(ui)
160139
{
161140
case ui_message_handlert::uit::PLAIN:
162-
show_symbol_table_plain(symbol_table, std::cout);
141+
show_symbol_table_plain(symbol_table, std::cout, formatter);
163142
break;
164143

165144
case ui_message_handlert::uit::XML_UI:
166-
show_symbol_table_xml_ui();
145+
show_symbol_table_xml_ui(formatter);
167146
break;
168147

169148
default:
@@ -173,23 +152,25 @@ void show_symbol_table(
173152

174153
void show_symbol_table(
175154
const goto_modelt &goto_model,
176-
ui_message_handlert::uit ui)
155+
ui_message_handlert::uit ui,
156+
formattert &formatter)
177157
{
178-
show_symbol_table(goto_model.symbol_table, ui);
158+
show_symbol_table(goto_model.symbol_table, ui, formatter);
179159
}
180160

181161
void show_symbol_table_brief(
182162
const symbol_tablet &symbol_table,
183-
ui_message_handlert::uit ui)
163+
ui_message_handlert::uit ui,
164+
formattert &formatter)
184165
{
185166
switch(ui)
186167
{
187168
case ui_message_handlert::uit::PLAIN:
188-
show_symbol_table_brief_plain(symbol_table, std::cout);
169+
show_symbol_table_brief_plain(symbol_table, std::cout, formatter);
189170
break;
190171

191172
case ui_message_handlert::uit::XML_UI:
192-
show_symbol_table_xml_ui();
173+
show_symbol_table_xml_ui(formatter);
193174
break;
194175

195176
default:
@@ -199,7 +180,8 @@ void show_symbol_table_brief(
199180

200181
void show_symbol_table_brief(
201182
const goto_modelt &goto_model,
202-
ui_message_handlert::uit ui)
183+
ui_message_handlert::uit ui,
184+
formattert &formatter)
203185
{
204-
show_symbol_table_brief(goto_model.symbol_table, ui);
186+
show_symbol_table_brief(goto_model.symbol_table, ui, formatter);
205187
}

‎src/goto-programs/show_symbol_table.h

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,25 +12,30 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H
1313
#define CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H
1414

15+
#include <util/formatter.h>
1516
#include <util/ui_message.h>
1617

1718
class symbol_tablet;
1819
class goto_modelt;
1920

2021
void show_symbol_table(
2122
const symbol_tablet &,
22-
ui_message_handlert::uit ui);
23+
ui_message_handlert::uit ui,
24+
formattert & = debug_formatter);
2325

2426
void show_symbol_table_brief(
2527
const symbol_tablet &,
26-
ui_message_handlert::uit ui);
28+
ui_message_handlert::uit ui,
29+
formattert & = debug_formatter);
2730

2831
void show_symbol_table(
2932
const goto_modelt &,
30-
ui_message_handlert::uit ui);
33+
ui_message_handlert::uit ui,
34+
formattert & = debug_formatter);
3135

3236
void show_symbol_table_brief(
3337
const goto_modelt &,
34-
ui_message_handlert::uit ui);
38+
ui_message_handlert::uit ui,
39+
formattert & = debug_formatter);
3540

3641
#endif // CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H

‎src/jbmc/jbmc_parse_options.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ Author: Daniel Kroening, [email protected]
5555
#include <java_bytecode/convert_java_nondet.h>
5656
#include <java_bytecode/java_bytecode_language.h>
5757
#include <java_bytecode/java_enum_static_init_unwind_handler.h>
58+
#include <java_bytecode/java_formatter.h>
5859
#include <java_bytecode/remove_exceptions.h>
5960
#include <java_bytecode/remove_instanceof.h>
6061
#include <java_bytecode/remove_java_new.h>
@@ -671,8 +672,10 @@ int jbmc_parse_optionst::get_goto_program(
671672
// values, etc
672673
if(cmdline.isset("show-symbol-table"))
673674
{
675+
const namespacet ns(lazy_goto_model.symbol_table);
676+
java_formattert formatter(ns);
674677
show_symbol_table(
675-
lazy_goto_model.symbol_table, ui_message_handler.get_ui());
678+
lazy_goto_model.symbol_table, ui_message_handler.get_ui(), formatter);
676679
return 0;
677680
}
678681

@@ -850,8 +853,10 @@ bool jbmc_parse_optionst::show_loaded_functions(
850853
{
851854
if(cmdline.isset("show-symbol-table"))
852855
{
856+
namespacet ns(goto_model.get_symbol_table());
857+
java_formattert formatter(ns);
853858
show_symbol_table(
854-
goto_model.get_symbol_table(), ui_message_handler.get_ui());
859+
goto_model.get_symbol_table(), ui_message_handler.get_ui(), formatter);
855860
return true;
856861
}
857862

0 commit comments

Comments
 (0)