From 3de66f813a64c2e86f4fdd50359500c3d4da4b61 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Jan 2019 19:40:08 +0000 Subject: [PATCH 1/4] Make order of arguments in ai_baset::output* consistent Place the identifier (the name of the function) before the goto program. --- src/analyses/ai.cpp | 18 +++++++++--------- src/analyses/ai.h | 18 +++++++++--------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 0de2c06bf2c..0a094c73fa8 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -35,15 +35,15 @@ void ai_baset::output( out << "////\n"; out << "\n"; - output(ns, f_it->second.body, f_it->first, out); + output(ns, f_it->first, f_it->second.body, out); } } } void ai_baset::output( const namespacet &ns, - const goto_programt &goto_program, const irep_idt &identifier, + const goto_programt &goto_program, std::ostream &out) const { forall_goto_program_instructions(i_it, goto_program) @@ -70,8 +70,8 @@ jsont ai_baset::output_json( { if(f_it->second.body_available()) { - result[id2string(f_it->first)]= - output_json(ns, f_it->second.body, f_it->first); + result[id2string(f_it->first)] = + output_json(ns, f_it->first, f_it->second.body); } else { @@ -90,8 +90,8 @@ jsont ai_baset::output_json( /// \return The JSON object jsont ai_baset::output_json( const namespacet &ns, - const goto_programt &goto_program, - const irep_idt &identifier) const + const irep_idt &identifier, + const goto_programt &goto_program) const { json_arrayt contents; @@ -129,7 +129,7 @@ xmlt ai_baset::output_xml( if(f_it->second.body_available()) { - function.new_element(output_xml(ns, f_it->second.body, f_it->first)); + function.new_element(output_xml(ns, f_it->first, f_it->second.body)); } program.new_element(function); @@ -146,8 +146,8 @@ xmlt ai_baset::output_xml( /// \return The XML object xmlt ai_baset::output_xml( const namespacet &ns, - const goto_programt &goto_program, - const irep_idt &identifier) const + const irep_idt &identifier, + const goto_programt &goto_program) const { xmlt function_body; diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 9ea73b8ebb9..09a29614696 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -145,7 +145,7 @@ class ai_baset const goto_programt &goto_program, std::ostream &out) const { - output(ns, goto_program, "", out); + output(ns, "", goto_program, out); } /// Output the abstract states for a function @@ -154,7 +154,7 @@ class ai_baset const goto_functionst::goto_functiont &goto_function, std::ostream &out) const { - output(ns, goto_function.body, "", out); + output(ns, "", goto_function.body, out); } /// Output the abstract states for the whole program as JSON @@ -175,7 +175,7 @@ class ai_baset const namespacet &ns, const goto_programt &goto_program) const { - return output_json(ns, goto_program, ""); + return output_json(ns, "", goto_program); } /// Output the abstract states for a single function as JSON @@ -183,7 +183,7 @@ class ai_baset const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const { - return output_json(ns, goto_function.body, ""); + return output_json(ns, "", goto_function.body); } /// Output the abstract states for the whole program as XML @@ -204,7 +204,7 @@ class ai_baset const namespacet &ns, const goto_programt &goto_program) const { - return output_xml(ns, goto_program, ""); + return output_xml(ns, "", goto_program); } /// Output the abstract states for a single function as XML @@ -259,8 +259,8 @@ class ai_baset /// \return The JSON object virtual jsont output_json( const namespacet &ns, - const goto_programt &goto_program, - const irep_idt &identifier) const; + const irep_idt &identifier, + const goto_programt &goto_program) const; /// Output the abstract states for a single function as XML /// \param ns: The namespace @@ -270,8 +270,8 @@ class ai_baset /// \return The XML object virtual xmlt output_xml( const namespacet &ns, - const goto_programt &goto_program, - const irep_idt &identifier) const; + const irep_idt &identifier, + const goto_programt &goto_program) const; /// The work queue, sorted by location number typedef std::map working_sett; From cc82d5ce8f9bc18250fdfca68051ff8b5e22984a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Jan 2019 19:41:41 +0000 Subject: [PATCH 2/4] 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. --- src/analyses/ai.cpp | 10 ++++++---- src/analyses/ai.h | 14 +++++++++----- src/analyses/dependence_graph.h | 7 +++---- src/analyses/invariant_propagation.cpp | 8 +++++--- src/analyses/invariant_propagation.h | 3 ++- 5 files changed, 25 insertions(+), 17 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 0a094c73fa8..d583a1a86ab 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -187,12 +187,14 @@ void ai_baset::entry_state(const goto_programt &goto_program) get_state(goto_program.instructions.begin()).make_entry(); } -void ai_baset::initialize(const goto_functionst::goto_functiont &goto_function) +void ai_baset::initialize( + const irep_idt &function_identifier, + const goto_functionst::goto_functiont &goto_function) { - initialize(goto_function.body); + initialize(function, goto_function.body); } -void ai_baset::initialize(const goto_programt &goto_program) +void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program) { // we mark everything as unreachable as starting point @@ -203,7 +205,7 @@ void ai_baset::initialize(const goto_programt &goto_program) void ai_baset::initialize(const goto_functionst &goto_functions) { forall_goto_functions(it, goto_functions) - initialize(it->second); + initialize(it->first, it->second); } void ai_baset::finalize() diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 09a29614696..1cab7bea6a9 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -50,7 +50,7 @@ class ai_baset const namespacet &ns) { goto_functionst goto_functions; - initialize(goto_program); + initialize(function_identifier, goto_program); entry_state(goto_program); fixedpoint(function_identifier, goto_program, goto_functions, ns); finalize(); @@ -84,7 +84,7 @@ class ai_baset const namespacet &ns) { goto_functionst goto_functions; - initialize(goto_function); + initialize(function_identifier, goto_function); entry_state(goto_function.body); fixedpoint(function_identifier, goto_function.body, goto_functions, ns); finalize(); @@ -212,16 +212,20 @@ class ai_baset const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const { - return output_xml(ns, goto_function.body, ""); + return output_xml(ns, "", goto_function.body); } protected: /// Initialize all the abstract states for a single function. Override this to /// do custom per-domain initialization. - virtual void initialize(const goto_programt &goto_program); + virtual void initialize( + const irep_idt &function_identifier, + const goto_programt &goto_program); /// Initialize all the abstract states for a single function. - virtual void initialize(const goto_functionst::goto_functiont &goto_function); + virtual void initialize( + const irep_idt &function_identifier, + const goto_functionst::goto_functiont &goto_function); /// Initialize all the abstract states for a whole program. Override this to /// do custom per-analysis initialization. diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index d7a8b6c1340..64346940b4b 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -236,14 +236,13 @@ class dependence_grapht: rd(goto_functions, ns); } - void initialize(const goto_programt &goto_program) + void initialize(const irep_idt &function, const goto_programt &goto_program) { - ait::initialize(goto_program); + ait::initialize(function, goto_program); if(!goto_program.empty()) { - const irep_idt id=goto_programt::get_function_id(goto_program); - cfg_post_dominatorst &pd=post_dominators[id]; + cfg_post_dominatorst &pd = post_dominators[function]; pd(goto_program); } } diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index 04cd526b7d6..7cbe50da306 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -202,9 +202,11 @@ bool invariant_propagationt::check_type(const typet &type) const return false; } -void invariant_propagationt::initialize(const goto_programt &goto_program) +void invariant_propagationt::initialize( + const irep_idt &function, + const goto_programt &goto_program) { - baset::initialize(goto_program); + baset::initialize(function, goto_program); forall_goto_program_instructions(it, goto_program) { @@ -228,7 +230,7 @@ void invariant_propagationt::initialize(const goto_functionst &goto_functions) baset::initialize(goto_functions); forall_goto_functions(f_it, goto_functions) - initialize(f_it->second.body); + initialize(f_it->first, f_it->second.body); } void invariant_propagationt::simplify(goto_functionst &goto_functions) diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h index d21f6373bcb..dd33b0b68d4 100644 --- a/src/analyses/invariant_propagation.h +++ b/src/analyses/invariant_propagation.h @@ -36,7 +36,8 @@ class invariant_propagationt:public return (*this)[l].invariant_set; } - virtual void initialize(const goto_programt &goto_program); + virtual void + initialize(const irep_idt &function, const goto_programt &goto_program); virtual void initialize(const goto_functionst &goto_functions); void make_all_true(); From 63e00babbb3ddcf860a2f99b84bf2ed985577371 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 9 Oct 2018 14:55:16 +0100 Subject: [PATCH 3/4] ai_baset: output now requires function identifier 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. --- src/analyses/ai.cpp | 24 ++++---------- src/analyses/ai.h | 45 +++++++++++---------------- src/goto-instrument/uninitialized.cpp | 2 +- 3 files changed, 25 insertions(+), 46 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index d583a1a86ab..6995bb190dc 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -42,7 +42,7 @@ void ai_baset::output( void ai_baset::output( const namespacet &ns, - const irep_idt &identifier, + const irep_idt &function_identifier, const goto_programt &goto_program, std::ostream &out) const { @@ -54,7 +54,7 @@ void ai_baset::output( abstract_state_before(i_it)->output(out, *this, ns); out << "\n"; #if 1 - goto_program.output_instruction(ns, identifier, out, *i_it); + goto_program.output_instruction(ns, function_identifier, out, *i_it); out << "\n"; #endif } @@ -82,15 +82,9 @@ jsont ai_baset::output_json( return std::move(result); } -/// Output the domains for a single function as JSON -/// \param ns: The namespace -/// \param goto_program: The goto program -/// \param identifier: The identifier used to find a symbol to identify the -/// source language -/// \return The JSON object jsont ai_baset::output_json( const namespacet &ns, - const irep_idt &identifier, + const irep_idt &function_identifier, const goto_programt &goto_program) const { json_arrayt contents; @@ -99,7 +93,7 @@ jsont ai_baset::output_json( { // Ideally we need output_instruction_json std::ostringstream out; - goto_program.output_instruction(ns, identifier, out, *i_it); + goto_program.output_instruction(ns, function_identifier, out, *i_it); json_objectt location( {{"locationNumber", json_numbert(std::to_string(i_it->location_number))}, @@ -138,15 +132,9 @@ xmlt ai_baset::output_xml( return program; } -/// Output the domains for a single function as XML -/// \param ns: The namespace -/// \param goto_program: The goto program -/// \param identifier: The identifier used to find a symbol to identify the -/// source language -/// \return The XML object xmlt ai_baset::output_xml( const namespacet &ns, - const irep_idt &identifier, + const irep_idt &function_identifier, const goto_programt &goto_program) const { xmlt function_body; @@ -161,7 +149,7 @@ xmlt ai_baset::output_xml( // Ideally we need output_instruction_xml std::ostringstream out; - goto_program.output_instruction(ns, identifier, out, *i_it); + goto_program.output_instruction(ns, function_identifier, out, *i_it); location.set_attribute("instruction", out.str()); function_body.new_element(location); diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 1cab7bea6a9..0f8521a79c9 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -124,6 +124,18 @@ class ai_baset { } + /// Output the abstract states for a single function + /// \param ns: The namespace + /// \param function_identifier: The identifier used to find a symbol to + /// identify the \p goto_program's source language + /// \param goto_program: The goto program + /// \param out: The ostream to direct output to + virtual void output( + const namespacet &ns, + const irep_idt &function_identifier, + const goto_programt &goto_program, + std::ostream &out) const; + /// Output the abstract states for a whole program virtual void output( const namespacet &ns, @@ -139,15 +151,6 @@ class ai_baset output(ns, goto_model.goto_functions, out); } - /// Output the abstract states for a function - void output( - const namespacet &ns, - const goto_programt &goto_program, - std::ostream &out) const - { - output(ns, "", goto_program, out); - } - /// Output the abstract states for a function void output( const namespacet &ns, @@ -243,38 +246,26 @@ class ai_baset /// entry state required by the analysis void entry_state(const goto_functionst &goto_functions); - /// Output the abstract states for a single function - /// \param ns: The namespace - /// \param goto_program: The goto program - /// \param identifier: The identifier used to find a symbol to identify the - /// source language - /// \param out: The ostream to direct output to - virtual void output( - const namespacet &ns, - const goto_programt &goto_program, - const irep_idt &identifier, - std::ostream &out) const; - /// Output the abstract states for a single function as JSON /// \param ns: The namespace /// \param goto_program: The goto program - /// \param identifier: The identifier used to find a symbol to identify the - /// source language + /// \param function_identifier: The identifier used to find a symbol to + /// identify the source language /// \return The JSON object virtual jsont output_json( const namespacet &ns, - const irep_idt &identifier, + const irep_idt &function_identifier, const goto_programt &goto_program) const; /// Output the abstract states for a single function as XML /// \param ns: The namespace /// \param goto_program: The goto program - /// \param identifier: The identifier used to find a symbol to identify the - /// source language + /// \param function_identifier: The identifier used to find a symbol to + /// identify the source language /// \return The XML object virtual xmlt output_xml( const namespacet &ns, - const irep_idt &identifier, + const irep_idt &function_identifier, const goto_programt &goto_program) const; /// The work queue, sorted by location number diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 1c5e85b68fc..701485949d3 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -223,7 +223,7 @@ void show_uninitialized( out << "////\n\n"; uninitialized_analysist uninitialized_analysis; uninitialized_analysis(f_it->first, f_it->second.body, ns); - uninitialized_analysis.output(ns, f_it->second.body, out); + uninitialized_analysis.output(ns, f_it->first, f_it->second.body, out); } } } From d7db14f8ecf9f5e62166f77f1ebbf43aca0149ae Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 20 Jan 2019 10:29:45 +0000 Subject: [PATCH 4/4] ai_baset: consistently use function_id instead of function_identifier It is as clear, but makes for shorter lines. --- src/analyses/ai.cpp | 59 ++++++++++++++++++--------------------------- src/analyses/ai.h | 39 +++++++++++++++--------------- 2 files changed, 42 insertions(+), 56 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 6995bb190dc..d20c0c4ebbe 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -42,7 +42,7 @@ void ai_baset::output( void ai_baset::output( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const { @@ -54,7 +54,7 @@ void ai_baset::output( abstract_state_before(i_it)->output(out, *this, ns); out << "\n"; #if 1 - goto_program.output_instruction(ns, function_identifier, out, *i_it); + goto_program.output_instruction(ns, function_id, out, *i_it); out << "\n"; #endif } @@ -84,7 +84,7 @@ jsont ai_baset::output_json( jsont ai_baset::output_json( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program) const { json_arrayt contents; @@ -93,7 +93,7 @@ jsont ai_baset::output_json( { // Ideally we need output_instruction_json std::ostringstream out; - goto_program.output_instruction(ns, function_identifier, out, *i_it); + goto_program.output_instruction(ns, function_id, out, *i_it); json_objectt location( {{"locationNumber", json_numbert(std::to_string(i_it->location_number))}, @@ -134,7 +134,7 @@ xmlt ai_baset::output_xml( xmlt ai_baset::output_xml( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program) const { xmlt function_body; @@ -149,7 +149,7 @@ xmlt ai_baset::output_xml( // Ideally we need output_instruction_xml std::ostringstream out; - goto_program.output_instruction(ns, function_identifier, out, *i_it); + goto_program.output_instruction(ns, function_id, out, *i_it); location.set_attribute("instruction", out.str()); function_body.new_element(location); @@ -176,10 +176,10 @@ void ai_baset::entry_state(const goto_programt &goto_program) } void ai_baset::initialize( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) { - initialize(function, goto_function.body); + initialize(function_id, goto_function.body); } void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program) @@ -214,7 +214,7 @@ ai_baset::locationt ai_baset::get_next( } bool ai_baset::fixedpoint( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) @@ -234,8 +234,7 @@ bool ai_baset::fixedpoint( locationt l=get_next(working_set); // goto_program is really only needed for iterator manipulation - if(visit( - function_identifier, l, working_set, goto_program, goto_functions, ns)) + if(visit(function_id, l, working_set, goto_program, goto_functions, ns)) new_data=true; } @@ -243,7 +242,7 @@ bool ai_baset::fixedpoint( } bool ai_baset::visit( - const irep_idt &function_identifier, + const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, @@ -274,7 +273,7 @@ bool ai_baset::visit( to_code_function_call(l->code); if(do_function_call_rec( - function_identifier, + function_id, l, to_l, code.function(), @@ -288,8 +287,7 @@ bool ai_baset::visit( // initialize state, if necessary get_state(to_l); - new_values.transform( - function_identifier, l, function_identifier, to_l, *this, ns); + new_values.transform(function_id, l, function_id, to_l, *this, ns); if(merge(new_values, l, to_l)) have_new_values=true; @@ -306,7 +304,7 @@ bool ai_baset::visit( } bool ai_baset::do_function_call( - const irep_idt &calling_function_identifier, + const irep_idt &calling_function_id, locationt l_call, locationt l_return, const goto_functionst &goto_functions, @@ -327,12 +325,7 @@ bool ai_baset::do_function_call( // If we don't have a body, we just do an edge call -> return std::unique_ptr tmp_state(make_temporary_state(get_state(l_call))); tmp_state->transform( - calling_function_identifier, - l_call, - calling_function_identifier, - l_return, - *this, - ns); + calling_function_id, l_call, calling_function_id, l_return, *this, ns); return merge(*tmp_state, l_call, l_return); } @@ -350,7 +343,7 @@ bool ai_baset::do_function_call( // do the edge from the call site to the beginning of the function std::unique_ptr tmp_state(make_temporary_state(get_state(l_call))); tmp_state->transform( - calling_function_identifier, l_call, f_it->first, l_begin, *this, ns); + calling_function_id, l_call, f_it->first, l_begin, *this, ns); bool new_data=false; @@ -378,7 +371,7 @@ bool ai_baset::do_function_call( std::unique_ptr tmp_state(make_temporary_state(end_state)); tmp_state->transform( - f_it->first, l_end, calling_function_identifier, l_return, *this, ns); + f_it->first, l_end, calling_function_id, l_return, *this, ns); // Propagate those return merge(*tmp_state, l_end, l_return); @@ -386,7 +379,7 @@ bool ai_baset::do_function_call( } bool ai_baset::do_function_call_rec( - const irep_idt &calling_function_identifier, + const irep_idt &calling_function_id, locationt l_call, locationt l_return, const exprt &function, @@ -414,13 +407,7 @@ bool ai_baset::do_function_call_rec( "Function " + id2string(identifier) + "not in function map"); new_data = do_function_call( - calling_function_identifier, - l_call, - l_return, - goto_functions, - it, - arguments, - ns); + calling_function_id, l_call, l_return, goto_functions, it, arguments, ns); return new_data; } @@ -454,16 +441,16 @@ void ai_baset::concurrent_fixedpoint( struct wl_entryt { wl_entryt( - const irep_idt &_function_identifier, + const irep_idt &_function_id, const goto_programt &_goto_program, locationt _location) - : function_identifier(_function_identifier), + : function_id(_function_id), goto_program(&_goto_program), location(_location) { } - irep_idt function_identifier; + irep_idt function_id; const goto_programt *goto_program; locationt location; }; @@ -506,7 +493,7 @@ void ai_baset::concurrent_fixedpoint( goto_programt::const_targett l=get_next(working_set); visit( - wl_entry.function_identifier, + wl_entry.function_id, l, working_set, *(wl_entry.goto_program), diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 0f8521a79c9..784cfa09af6 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -45,14 +45,14 @@ class ai_baset /// Run abstract interpretation on a single function void operator()( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns) { goto_functionst goto_functions; - initialize(function_identifier, goto_program); + initialize(function_id, goto_program); entry_state(goto_program); - fixedpoint(function_identifier, goto_program, goto_functions, ns); + fixedpoint(function_id, goto_program, goto_functions, ns); finalize(); } @@ -79,14 +79,14 @@ class ai_baset /// Run abstract interpretation on a single function void operator()( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) { goto_functionst goto_functions; - initialize(function_identifier, goto_function); + initialize(function_id, goto_function); entry_state(goto_function.body); - fixedpoint(function_identifier, goto_function.body, goto_functions, ns); + fixedpoint(function_id, goto_function.body, goto_functions, ns); finalize(); } @@ -126,13 +126,13 @@ class ai_baset /// Output the abstract states for a single function /// \param ns: The namespace - /// \param function_identifier: The identifier used to find a symbol to + /// \param function_id: The identifier used to find a symbol to /// identify the \p goto_program's source language /// \param goto_program: The goto program /// \param out: The ostream to direct output to virtual void output( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const; @@ -221,13 +221,12 @@ class ai_baset protected: /// Initialize all the abstract states for a single function. Override this to /// do custom per-domain initialization. - virtual void initialize( - const irep_idt &function_identifier, - const goto_programt &goto_program); + virtual void + initialize(const irep_idt &function_id, const goto_programt &goto_program); /// Initialize all the abstract states for a single function. virtual void initialize( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function); /// Initialize all the abstract states for a whole program. Override this to @@ -249,23 +248,23 @@ class ai_baset /// Output the abstract states for a single function as JSON /// \param ns: The namespace /// \param goto_program: The goto program - /// \param function_identifier: The identifier used to find a symbol to + /// \param function_id: The identifier used to find a symbol to /// identify the source language /// \return The JSON object virtual jsont output_json( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program) const; /// Output the abstract states for a single function as XML /// \param ns: The namespace /// \param goto_program: The goto program - /// \param function_identifier: The identifier used to find a symbol to + /// \param function_id: The identifier used to find a symbol to /// identify the source language /// \return The XML object virtual xmlt output_xml( const namespacet &ns, - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program) const; /// The work queue, sorted by location number @@ -285,7 +284,7 @@ class ai_baset /// Run the fixedpoint algorithm until it reaches a fixed point /// \return True if we found something new bool fixedpoint( - const irep_idt &function_identifier, + const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns); @@ -307,7 +306,7 @@ class ai_baset /// or applications of the abstract transformer /// \return True if the state was changed bool visit( - const irep_idt &function_identifier, + const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, @@ -316,7 +315,7 @@ class ai_baset // function calls bool do_function_call_rec( - const irep_idt &calling_function_identifier, + const irep_idt &calling_function_id, locationt l_call, locationt l_return, const exprt &function, @@ -325,7 +324,7 @@ class ai_baset const namespacet &ns); bool do_function_call( - const irep_idt &calling_function_identifier, + const irep_idt &calling_function_id, locationt l_call, locationt l_return, const goto_functionst &goto_functions,