@@ -42,7 +42,7 @@ void ai_baset::output(
42
42
43
43
void ai_baset::output (
44
44
const namespacet &ns,
45
- const irep_idt &function_identifier ,
45
+ const irep_idt &function_id ,
46
46
const goto_programt &goto_program,
47
47
std::ostream &out) const
48
48
{
@@ -54,7 +54,7 @@ void ai_baset::output(
54
54
abstract_state_before (i_it)->output (out, *this , ns);
55
55
out << " \n " ;
56
56
#if 1
57
- goto_program.output_instruction (ns, function_identifier , out, *i_it);
57
+ goto_program.output_instruction (ns, function_id , out, *i_it);
58
58
out << " \n " ;
59
59
#endif
60
60
}
@@ -84,7 +84,7 @@ jsont ai_baset::output_json(
84
84
85
85
jsont ai_baset::output_json (
86
86
const namespacet &ns,
87
- const irep_idt &function_identifier ,
87
+ const irep_idt &function_id ,
88
88
const goto_programt &goto_program) const
89
89
{
90
90
json_arrayt contents;
@@ -93,7 +93,7 @@ jsont ai_baset::output_json(
93
93
{
94
94
// Ideally we need output_instruction_json
95
95
std::ostringstream out;
96
- goto_program.output_instruction (ns, function_identifier , out, *i_it);
96
+ goto_program.output_instruction (ns, function_id , out, *i_it);
97
97
98
98
json_objectt location (
99
99
{{" locationNumber" , json_numbert (std::to_string (i_it->location_number ))},
@@ -134,7 +134,7 @@ xmlt ai_baset::output_xml(
134
134
135
135
xmlt ai_baset::output_xml (
136
136
const namespacet &ns,
137
- const irep_idt &function_identifier ,
137
+ const irep_idt &function_id ,
138
138
const goto_programt &goto_program) const
139
139
{
140
140
xmlt function_body;
@@ -149,7 +149,7 @@ xmlt ai_baset::output_xml(
149
149
150
150
// Ideally we need output_instruction_xml
151
151
std::ostringstream out;
152
- goto_program.output_instruction (ns, function_identifier , out, *i_it);
152
+ goto_program.output_instruction (ns, function_id , out, *i_it);
153
153
location.set_attribute (" instruction" , out.str ());
154
154
155
155
function_body.new_element (location);
@@ -176,10 +176,10 @@ void ai_baset::entry_state(const goto_programt &goto_program)
176
176
}
177
177
178
178
void ai_baset::initialize (
179
- const irep_idt &function_identifier ,
179
+ const irep_idt &function_id ,
180
180
const goto_functionst::goto_functiont &goto_function)
181
181
{
182
- initialize (function , goto_function.body );
182
+ initialize (function_id , goto_function.body );
183
183
}
184
184
185
185
void ai_baset::initialize (const irep_idt &, const goto_programt &goto_program)
@@ -214,7 +214,7 @@ ai_baset::locationt ai_baset::get_next(
214
214
}
215
215
216
216
bool ai_baset::fixedpoint (
217
- const irep_idt &function_identifier ,
217
+ const irep_idt &function_id ,
218
218
const goto_programt &goto_program,
219
219
const goto_functionst &goto_functions,
220
220
const namespacet &ns)
@@ -234,16 +234,15 @@ bool ai_baset::fixedpoint(
234
234
locationt l=get_next (working_set);
235
235
236
236
// goto_program is really only needed for iterator manipulation
237
- if (visit (
238
- function_identifier, l, working_set, goto_program, goto_functions, ns))
237
+ if (visit (function_id, l, working_set, goto_program, goto_functions, ns))
239
238
new_data=true ;
240
239
}
241
240
242
241
return new_data;
243
242
}
244
243
245
244
bool ai_baset::visit (
246
- const irep_idt &function_identifier ,
245
+ const irep_idt &function_id ,
247
246
locationt l,
248
247
working_sett &working_set,
249
248
const goto_programt &goto_program,
@@ -274,7 +273,7 @@ bool ai_baset::visit(
274
273
to_code_function_call (l->code );
275
274
276
275
if (do_function_call_rec (
277
- function_identifier ,
276
+ function_id ,
278
277
l,
279
278
to_l,
280
279
code.function (),
@@ -288,8 +287,7 @@ bool ai_baset::visit(
288
287
// initialize state, if necessary
289
288
get_state (to_l);
290
289
291
- new_values.transform (
292
- function_identifier, l, function_identifier, to_l, *this , ns);
290
+ new_values.transform (function_id, l, function_id, to_l, *this , ns);
293
291
294
292
if (merge (new_values, l, to_l))
295
293
have_new_values=true ;
@@ -306,7 +304,7 @@ bool ai_baset::visit(
306
304
}
307
305
308
306
bool ai_baset::do_function_call (
309
- const irep_idt &calling_function_identifier ,
307
+ const irep_idt &calling_function_id ,
310
308
locationt l_call,
311
309
locationt l_return,
312
310
const goto_functionst &goto_functions,
@@ -327,12 +325,7 @@ bool ai_baset::do_function_call(
327
325
// If we don't have a body, we just do an edge call -> return
328
326
std::unique_ptr<statet> tmp_state (make_temporary_state (get_state (l_call)));
329
327
tmp_state->transform (
330
- calling_function_identifier,
331
- l_call,
332
- calling_function_identifier,
333
- l_return,
334
- *this ,
335
- ns);
328
+ calling_function_id, l_call, calling_function_id, l_return, *this , ns);
336
329
337
330
return merge (*tmp_state, l_call, l_return);
338
331
}
@@ -350,7 +343,7 @@ bool ai_baset::do_function_call(
350
343
// do the edge from the call site to the beginning of the function
351
344
std::unique_ptr<statet> tmp_state (make_temporary_state (get_state (l_call)));
352
345
tmp_state->transform (
353
- calling_function_identifier , l_call, f_it->first , l_begin, *this , ns);
346
+ calling_function_id , l_call, f_it->first , l_begin, *this , ns);
354
347
355
348
bool new_data=false ;
356
349
@@ -378,15 +371,15 @@ bool ai_baset::do_function_call(
378
371
379
372
std::unique_ptr<statet> tmp_state (make_temporary_state (end_state));
380
373
tmp_state->transform (
381
- f_it->first , l_end, calling_function_identifier , l_return, *this , ns);
374
+ f_it->first , l_end, calling_function_id , l_return, *this , ns);
382
375
383
376
// Propagate those
384
377
return merge (*tmp_state, l_end, l_return);
385
378
}
386
379
}
387
380
388
381
bool ai_baset::do_function_call_rec (
389
- const irep_idt &calling_function_identifier ,
382
+ const irep_idt &calling_function_id ,
390
383
locationt l_call,
391
384
locationt l_return,
392
385
const exprt &function,
@@ -414,13 +407,7 @@ bool ai_baset::do_function_call_rec(
414
407
" Function " + id2string (identifier) + " not in function map" );
415
408
416
409
new_data = do_function_call (
417
- calling_function_identifier,
418
- l_call,
419
- l_return,
420
- goto_functions,
421
- it,
422
- arguments,
423
- ns);
410
+ calling_function_id, l_call, l_return, goto_functions, it, arguments, ns);
424
411
425
412
return new_data;
426
413
}
@@ -454,16 +441,16 @@ void ai_baset::concurrent_fixedpoint(
454
441
struct wl_entryt
455
442
{
456
443
wl_entryt (
457
- const irep_idt &_function_identifier ,
444
+ const irep_idt &_function_id ,
458
445
const goto_programt &_goto_program,
459
446
locationt _location)
460
- : function_identifier(_function_identifier ),
447
+ : function_id(_function_id ),
461
448
goto_program (&_goto_program),
462
449
location(_location)
463
450
{
464
451
}
465
452
466
- irep_idt function_identifier ;
453
+ irep_idt function_id ;
467
454
const goto_programt *goto_program;
468
455
locationt location;
469
456
};
@@ -506,7 +493,7 @@ void ai_baset::concurrent_fixedpoint(
506
493
goto_programt::const_targett l=get_next (working_set);
507
494
508
495
visit (
509
- wl_entry.function_identifier ,
496
+ wl_entry.function_id ,
510
497
l,
511
498
working_set,
512
499
*(wl_entry.goto_program ),
0 commit comments