Skip to content

Commit a9d181f

Browse files
author
Daniel Kroening
committed
ai_baset: output now requires function identifier
1 parent 068f878 commit a9d181f

File tree

3 files changed

+19
-65
lines changed

3 files changed

+19
-65
lines changed

src/analyses/ai.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -35,15 +35,15 @@ void ai_baset::output(
3535
out << "////\n";
3636
out << "\n";
3737

38-
output(ns, f_it->second.body, f_it->first, out);
38+
output(ns, f_it->first, f_it->second.body, out);
3939
}
4040
}
4141
}
4242

4343
void ai_baset::output(
4444
const namespacet &ns,
45+
const irep_idt &function_identifier,
4546
const goto_programt &goto_program,
46-
const irep_idt &identifier,
4747
std::ostream &out) const
4848
{
4949
forall_goto_program_instructions(i_it, goto_program)
@@ -54,7 +54,7 @@ void ai_baset::output(
5454
abstract_state_before(i_it)->output(out, *this, ns);
5555
out << "\n";
5656
#if 1
57-
goto_program.output_instruction(ns, identifier, out, *i_it);
57+
goto_program.output_instruction(ns, function_identifier, out, *i_it);
5858
out << "\n";
5959
#endif
6060
}
@@ -74,7 +74,7 @@ jsont ai_baset::output_json(
7474
if(f_it->second.body_available())
7575
{
7676
result[id2string(f_it->first)]=
77-
output_json(ns, f_it->second.body, f_it->first);
77+
output_json(ns, f_it->first, f_it->second.body);
7878
}
7979
else
8080
{
@@ -90,8 +90,8 @@ jsont ai_baset::output_json(
9090
/// \return The JSON object
9191
jsont ai_baset::output_json(
9292
const namespacet &ns,
93-
const goto_programt &goto_program,
94-
const irep_idt &identifier) const
93+
const irep_idt &function,
94+
const goto_programt &goto_program) const
9595
{
9696
json_arrayt contents;
9797

@@ -107,7 +107,7 @@ jsont ai_baset::output_json(
107107

108108
// Ideally we need output_instruction_json
109109
std::ostringstream out;
110-
goto_program.output_instruction(ns, identifier, out, *i_it);
110+
goto_program.output_instruction(ns, function, out, *i_it);
111111
location["instruction"]=json_stringt(out.str());
112112

113113
contents.push_back(location);
@@ -135,7 +135,7 @@ xmlt ai_baset::output_xml(
135135

136136
if(f_it->second.body_available())
137137
{
138-
function.new_element(output_xml(ns, f_it->second.body, f_it->first));
138+
function.new_element(output_xml(ns, f_it->first, f_it->second.body));
139139
}
140140

141141
program.new_element(function);
@@ -149,8 +149,8 @@ xmlt ai_baset::output_xml(
149149
/// \return The XML object
150150
xmlt ai_baset::output_xml(
151151
const namespacet &ns,
152-
const goto_programt &goto_program,
153-
const irep_idt &identifier) const
152+
const irep_idt &function,
153+
const goto_programt &goto_program) const
154154
{
155155
xmlt function_body;
156156

@@ -168,7 +168,7 @@ xmlt ai_baset::output_xml(
168168

169169
// Ideally we need output_instruction_xml
170170
std::ostringstream out;
171-
goto_program.output_instruction(ns, identifier, out, *i_it);
171+
goto_program.output_instruction(ns, function, out, *i_it);
172172
location.set_attribute("instruction", out.str());
173173

174174
function_body.new_element(location);

src/analyses/ai.h

Lines changed: 7 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -112,22 +112,11 @@ class ai_baset
112112
output(ns, goto_model.goto_functions, out);
113113
}
114114

115-
void output(
115+
virtual void output(
116116
const namespacet &ns,
117+
const irep_idt &function,
117118
const goto_programt &goto_program,
118-
std::ostream &out) const
119-
{
120-
output(ns, goto_program, "", out);
121-
}
122-
123-
void output(
124-
const namespacet &ns,
125-
const goto_functionst::goto_functiont &goto_function,
126-
std::ostream &out) const
127-
{
128-
output(ns, goto_function.body, "", out);
129-
}
130-
119+
std::ostream &out) const;
131120

132121
virtual jsont output_json(
133122
const namespacet &ns,
@@ -140,21 +129,6 @@ class ai_baset
140129
return output_json(ns, goto_model.goto_functions);
141130
}
142131

143-
jsont output_json(
144-
const namespacet &ns,
145-
const goto_programt &goto_program) const
146-
{
147-
return output_json(ns, goto_program, "");
148-
}
149-
150-
jsont output_json(
151-
const namespacet &ns,
152-
const goto_functionst::goto_functiont &goto_function) const
153-
{
154-
return output_json(ns, goto_function.body, "");
155-
}
156-
157-
158132
virtual xmlt output_xml(
159133
const namespacet &ns,
160134
const goto_functionst &goto_functions) const;
@@ -166,20 +140,6 @@ class ai_baset
166140
return output_xml(ns, goto_model.goto_functions);
167141
}
168142

169-
xmlt output_xml(
170-
const namespacet &ns,
171-
const goto_programt &goto_program) const
172-
{
173-
return output_xml(ns, goto_program, "");
174-
}
175-
176-
xmlt output_xml(
177-
const namespacet &ns,
178-
const goto_functionst::goto_functiont &goto_function) const
179-
{
180-
return output_xml(ns, goto_function.body, "");
181-
}
182-
183143
protected:
184144
// overload to add a factory
185145
virtual void initialize(const goto_programt &);
@@ -192,21 +152,15 @@ class ai_baset
192152
void entry_state(const goto_programt &);
193153
void entry_state(const goto_functionst &);
194154

195-
virtual void output(
196-
const namespacet &ns,
197-
const goto_programt &goto_program,
198-
const irep_idt &identifier,
199-
std::ostream &out) const;
200-
201155
virtual jsont output_json(
202156
const namespacet &ns,
203-
const goto_programt &goto_program,
204-
const irep_idt &identifier) const;
157+
const irep_idt &function,
158+
const goto_programt &goto_program) const;
205159

206160
virtual xmlt output_xml(
207161
const namespacet &ns,
208-
const goto_programt &goto_program,
209-
const irep_idt &identifier) const;
162+
const irep_idt &function,
163+
const goto_programt &goto_program) const;
210164

211165

212166
// the work-queue is sorted by location number

src/goto-instrument/uninitialized.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,7 @@ void show_uninitialized(
223223
out << "////\n\n";
224224
uninitialized_analysist uninitialized_analysis;
225225
uninitialized_analysis(f_it->first, f_it->second.body, ns);
226-
uninitialized_analysis.output(ns, f_it->second.body, out);
226+
uninitialized_analysis.output(ns, f_it->first, f_it->second.body, out);
227227
}
228228
}
229229
}

0 commit comments

Comments
 (0)