Skip to content

Commit 286f5b2

Browse files
committed
ai_baset::initialize now requires a function name
We are working towards removing the "function" field from goto_programt::instructionst::instructiont, and thus need to pass the identifier of the function whenever it actually is required.
1 parent 1d71c5d commit 286f5b2

File tree

5 files changed

+25
-17
lines changed

5 files changed

+25
-17
lines changed

src/analyses/ai.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -187,12 +187,14 @@ void ai_baset::entry_state(const goto_programt &goto_program)
187187
get_state(goto_program.instructions.begin()).make_entry();
188188
}
189189

190-
void ai_baset::initialize(const goto_functionst::goto_functiont &goto_function)
190+
void ai_baset::initialize(
191+
const irep_idt &function_identifier,
192+
const goto_functionst::goto_functiont &goto_function)
191193
{
192-
initialize(goto_function.body);
194+
initialize(function, goto_function.body);
193195
}
194196

195-
void ai_baset::initialize(const goto_programt &goto_program)
197+
void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program)
196198
{
197199
// we mark everything as unreachable as starting point
198200

@@ -203,7 +205,7 @@ void ai_baset::initialize(const goto_programt &goto_program)
203205
void ai_baset::initialize(const goto_functionst &goto_functions)
204206
{
205207
forall_goto_functions(it, goto_functions)
206-
initialize(it->second);
208+
initialize(it->first, it->second);
207209
}
208210

209211
void ai_baset::finalize()

src/analyses/ai.h

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ class ai_baset
5050
const namespacet &ns)
5151
{
5252
goto_functionst goto_functions;
53-
initialize(goto_program);
53+
initialize(function_identifier, goto_program);
5454
entry_state(goto_program);
5555
fixedpoint(function_identifier, goto_program, goto_functions, ns);
5656
finalize();
@@ -84,7 +84,7 @@ class ai_baset
8484
const namespacet &ns)
8585
{
8686
goto_functionst goto_functions;
87-
initialize(goto_function);
87+
initialize(function_identifier, goto_function);
8888
entry_state(goto_function.body);
8989
fixedpoint(function_identifier, goto_function.body, goto_functions, ns);
9090
finalize();
@@ -212,16 +212,20 @@ class ai_baset
212212
const namespacet &ns,
213213
const goto_functionst::goto_functiont &goto_function) const
214214
{
215-
return output_xml(ns, goto_function.body, "");
215+
return output_xml(ns, "", goto_function.body);
216216
}
217217

218218
protected:
219219
/// Initialize all the abstract states for a single function. Override this to
220220
/// do custom per-domain initialization.
221-
virtual void initialize(const goto_programt &goto_program);
221+
virtual void initialize(
222+
const irep_idt &function_identifier,
223+
const goto_programt &goto_program);
222224

223225
/// Initialize all the abstract states for a single function.
224-
virtual void initialize(const goto_functionst::goto_functiont &goto_function);
226+
virtual void initialize(
227+
const irep_idt &function_identifier,
228+
const goto_functionst::goto_functiont &goto_function);
225229

226230
/// Initialize all the abstract states for a whole program. Override this to
227231
/// do custom per-analysis initialization.

src/analyses/dependence_graph.h

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -236,14 +236,13 @@ class dependence_grapht:
236236
rd(goto_functions, ns);
237237
}
238238

239-
void initialize(const goto_programt &goto_program)
239+
void initialize(const irep_idt &function, const goto_programt &goto_program)
240240
{
241-
ait<dep_graph_domaint>::initialize(goto_program);
241+
ait<dep_graph_domaint>::initialize(function, goto_program);
242242

243243
if(!goto_program.empty())
244244
{
245-
const irep_idt id=goto_programt::get_function_id(goto_program);
246-
cfg_post_dominatorst &pd=post_dominators[id];
245+
cfg_post_dominatorst &pd = post_dominators[function];
247246
pd(goto_program);
248247
}
249248
}

src/analyses/invariant_propagation.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -202,9 +202,11 @@ bool invariant_propagationt::check_type(const typet &type) const
202202
return false;
203203
}
204204

205-
void invariant_propagationt::initialize(const goto_programt &goto_program)
205+
void invariant_propagationt::initialize(
206+
const irep_idt &function,
207+
const goto_programt &goto_program)
206208
{
207-
baset::initialize(goto_program);
209+
baset::initialize(function, goto_program);
208210

209211
forall_goto_program_instructions(it, goto_program)
210212
{
@@ -228,7 +230,7 @@ void invariant_propagationt::initialize(const goto_functionst &goto_functions)
228230
baset::initialize(goto_functions);
229231

230232
forall_goto_functions(f_it, goto_functions)
231-
initialize(f_it->second.body);
233+
initialize(f_it->first, f_it->second.body);
232234
}
233235

234236
void invariant_propagationt::simplify(goto_functionst &goto_functions)

src/analyses/invariant_propagation.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ class invariant_propagationt:public
3636
return (*this)[l].invariant_set;
3737
}
3838

39-
virtual void initialize(const goto_programt &goto_program);
39+
virtual void
40+
initialize(const irep_idt &function, const goto_programt &goto_program);
4041
virtual void initialize(const goto_functionst &goto_functions);
4142

4243
void make_all_true();

0 commit comments

Comments
 (0)