From 8b7790aa927c8f3d16a79cad486bcd321b7ef578 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 11:31:14 +0000 Subject: [PATCH 01/14] Do not shadow "it" It's another iterator already in use, just rename this instance to "entry." --- src/goto-cc/linker_script_merge.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 78458bfd8a3..88579044870 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -480,11 +480,13 @@ int linker_script_merget::ls_data2instructions( symbol_exprt end_sym(d["end-symbol"].value, pointer_type(char_type())); linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end); - auto it=std::find_if(data["addresses"].array.begin(), - data["addresses"].array.end(), - [&d](const jsont &add) - { return add["sym"].value==d["end-symbol"].value; }); - if(it==data["addresses"].array.end()) + auto entry = std::find_if( + data["addresses"].array.begin(), + data["addresses"].array.end(), + [&d](const jsont &add) { + return add["sym"].value == d["end-symbol"].value; + }); + if(entry == data["addresses"].array.end()) { error() << "Could not find address corresponding to symbol '" << d["end-symbol"].value << "' (end of section)" << eom; @@ -493,9 +495,9 @@ int linker_script_merget::ls_data2instructions( source_locationt end_loc; end_loc.set_file(linker_script); std::ostringstream end_comment; - end_comment << "Pointer to end of object section '" - << d["section"].value << "'. Original address in object file" - << " is " << (*it)["val"].value; + end_comment << "Pointer to end of object section '" << d["section"].value + << "'. Original address in object file" + << " is " << (*entry)["val"].value; end_loc.set_comment(end_comment.str()); end_sym.add_source_location()=end_loc; From acec35555c2bd290db4392ece23d01852ea8086f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 11:32:52 +0000 Subject: [PATCH 02/14] Do not shadow "i_it" Renamed the first declaration, which really we don't use as an iterator. --- src/goto-instrument/nondet_static.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index c329763be2a..c786d848ef9 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -73,11 +73,11 @@ void nondet_static( goto_functionst &goto_functions, const irep_idt &fct_name) { - goto_functionst::function_mapt::iterator - i_it=goto_functions.function_map.find(fct_name); - assert(i_it!=goto_functions.function_map.end()); + goto_functionst::function_mapt::iterator fct_entry = + goto_functions.function_map.find(fct_name); + CHECK_RETURN(fct_entry != goto_functions.function_map.end()); - goto_programt &init=i_it->second.body; + goto_programt &init = fct_entry->second.body; Forall_goto_program_instructions(i_it, init) { From 3d75712527645de5322b5aec959cea9f2e5bbb6f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 12:07:19 +0000 Subject: [PATCH 03/14] Remove parameter "loop_counter" It is a class member, no need to pass it around as a parameter shadowing the very same reference. --- src/goto-instrument/accelerate/acceleration_utils.cpp | 5 +---- src/goto-instrument/accelerate/acceleration_utils.h | 3 --- .../accelerate/disjunctive_polynomial_acceleration.cpp | 2 +- src/goto-instrument/accelerate/polynomial_accelerator.cpp | 2 +- src/goto-instrument/accelerate/polynomial_accelerator.h | 1 - 5 files changed, 3 insertions(+), 10 deletions(-) diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index a04c5ef1a22..88a0c008f97 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -556,7 +556,6 @@ acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments( bool acceleration_utilst::do_arrays( goto_programt::instructionst &loop_body, std::map &polynomials, - exprt &loop_counter, substitutiont &substitution, scratch_programt &program) { @@ -881,7 +880,6 @@ bool acceleration_utilst::expr2poly( bool acceleration_utilst::do_nonrecursive( goto_programt::instructionst &body, std::map &polynomials, - exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program) @@ -1004,7 +1002,7 @@ bool acceleration_utilst::do_nonrecursive( const exprt &lhs=*it; const exprt &rhs=state[*it]; - if(!assign_array(lhs, rhs, loop_counter, program)) + if(!assign_array(lhs, rhs, program)) { #ifdef DEBUG std::cout << "Failed to assign a nonrecursive array: " << @@ -1020,7 +1018,6 @@ bool acceleration_utilst::do_nonrecursive( bool acceleration_utilst::assign_array( const exprt &lhs, const exprt &rhs, - const exprt &loop_counter, scratch_programt &program) { #ifdef DEBUG diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index 3d12c7db549..e2a77a46e47 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -101,7 +101,6 @@ class acceleration_utilst bool do_arrays(goto_programt::instructionst &loop_body, std::map &polynomials, - exprt &loop_counter, substitutiont &substitution, scratch_programt &program); expr_pairst gather_array_assignments( @@ -120,14 +119,12 @@ class acceleration_utilst bool do_nonrecursive( goto_programt::instructionst &loop_body, std::map &polynomials, - exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program); bool assign_array( const exprt &lhs, const exprt &rhs, - const exprt &loop_counter, scratch_programt &program); void gather_array_accesses(const exprt &expr, expr_sett &arrays); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index b94b616ea31..00e20612208 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -315,7 +315,7 @@ bool disjunctive_polynomial_accelerationt::accelerate( } // Add in any array assignments we can do now. - if(!utils.do_arrays(assigns, polynomials, loop_counter, stashed, program)) + if(!utils.do_arrays(assigns, polynomials, stashed, program)) { // We couldn't model some of the array assignments with polynomials... // Unfortunately that means we just have to bail out. diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 874b6f04639..2330e0eda59 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -251,7 +251,7 @@ bool polynomial_acceleratort::accelerate( // Add in any array assignments we can do now. if(!utils.do_nonrecursive( - assigns, polynomials, loop_counter, stashed, nonrecursive, program)) + assigns, polynomials, stashed, nonrecursive, program)) { // We couldn't model some of the array assignments with polynomials... // Unfortunately that means we just have to bail out. diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h index 8b92c0989ad..a9d2eb8ff40 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.h +++ b/src/goto-instrument/accelerate/polynomial_accelerator.h @@ -133,7 +133,6 @@ class polynomial_acceleratort bool do_arrays( goto_programt::instructionst &loop_body, std::map &polynomials, - exprt &loop_counter, substitutiont &substitution, scratch_programt &program); expr_pairst gather_array_assignments( From 14ac7055a7f5f90bb6b8b873995c7c0dc64c51c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 12:09:20 +0000 Subject: [PATCH 04/14] Avoid shadowing "it" Just use a ranged for instead. --- src/goto-instrument/accelerate/acceleration_utils.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 88a0c008f97..4ef547ca802 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -1242,12 +1242,8 @@ void acceleration_utilst::extract_polynomial( continue; } - for(expr_listt::iterator it=terms.begin(); - it!=terms.end(); - ++it) + for(const auto &term : terms) { - exprt term=*it; - if(degrees.find(term)!=degrees.end()) { degrees[term]++; From 39ac29381341fe3f82e71d5e66750149f37a50c1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 12:10:58 +0000 Subject: [PATCH 05/14] Avoid shadowing class member "subsumed" Renamed parameter to "subsumed_path". --- src/goto-instrument/accelerate/accelerate.cpp | 9 ++++++--- src/goto-instrument/accelerate/accelerate.h | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 355a6065191..62948970db2 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -183,15 +183,18 @@ void acceleratet::insert_accelerator( goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, - subsumed_patht &subsumed) + subsumed_patht &subsumed_path) { insert_looping_path( - loop_header, back_jump, accelerator.pure_accelerator, subsumed.accelerator); + loop_header, + back_jump, + accelerator.pure_accelerator, + subsumed_path.accelerator); if(!accelerator.overflow_path.instructions.empty()) { insert_looping_path( - loop_header, back_jump, accelerator.overflow_path, subsumed.residue); + loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue); } } diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h index 05dec188f28..9535852041b 100644 --- a/src/goto-instrument/accelerate/accelerate.h +++ b/src/goto-instrument/accelerate/accelerate.h @@ -84,7 +84,7 @@ class acceleratet goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, - subsumed_patht &subsumed); + subsumed_patht &subsumed_path); void set_dirty_vars(path_acceleratort &accelerator); void add_dirty_checks(); From e76b6dc8cf4a5b5b5b1efb47df755a690fc2c3bf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 13:21:30 +0000 Subject: [PATCH 06/14] Don't use both a static class member and a static local variable Having just one of these as "num_symbols" is sufficient. --- src/goto-instrument/accelerate/acceleration_utils.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index e2a77a46e47..c9213919376 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -154,8 +154,6 @@ class acceleration_utilst const goto_functionst &goto_functions; exprt &loop_counter; nil_exprt nil; - - static int num_symbols; }; #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H From 5e5bf6141ce2f4d52af8b284a4b18bd5dab51191 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 13:37:10 +0000 Subject: [PATCH 07/14] Use ranged for to avoid shadowing "it" Both cleanup (using ranged for) and fix of shadowing. --- src/goto-instrument/concurrency.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-instrument/concurrency.cpp index e2215da6bf2..49f91970fe8 100644 --- a/src/goto-instrument/concurrency.cpp +++ b/src/goto-instrument/concurrency.cpp @@ -130,8 +130,8 @@ void concurrency_instrumentationt::instrument( instrument(code.function()); // instrument(code.lhs(), LHS); - Forall_expr(it, code.arguments()) - instrument(*it); + for(auto &arg : code.arguments()) + instrument(arg); } } } From 5be52bac8d04630db04ae0ef1b2d89a7057afeca Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 13:38:22 +0000 Subject: [PATCH 08/14] Remove unused declaration It is never used and shadows a class member. --- src/goto-instrument/dot.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index 02bb5cf4148..5acaa52076e 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -264,8 +264,6 @@ void dott::output(std::ostream &out) out << "digraph G {\n"; out << DOTGRAPHSETTINGS << '\n'; - std::list clusters; - forall_goto_functions(it, goto_model.goto_functions) if(it->second.body_available()) write_dot_subgraph(out, id2string(it->first), it->second.body); From 97afec413d5414dc9e8c297c4bcad4e82765f8f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 13:40:10 +0000 Subject: [PATCH 09/14] Avoid shadowing "line" Rename the first declaration to "source_line" --- src/goto-instrument/document_properties.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp index d0cae86735e..b3a15283e7c 100644 --- a/src/goto-instrument/document_properties.cpp +++ b/src/goto-instrument/document_properties.cpp @@ -155,9 +155,9 @@ void document_propertiest::get_code( dest=""; const irep_idt &file=source_location.get_file(); - const irep_idt &line=source_location.get_line(); + const irep_idt &source_line = source_location.get_line(); - if(file=="" || line=="") + if(file == "" || source_line == "") return; std::ifstream in(id2string(file)); @@ -170,7 +170,7 @@ void document_propertiest::get_code( return; } - int line_int=unsafe_string2int(id2string(line)); + int line_int = unsafe_string2int(id2string(source_line)); int line_start=line_int-3, line_end=line_int+3; From 08903449b786dbb55ed1a003b313e0307ff40780 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 13:53:50 +0000 Subject: [PATCH 10/14] Avoid shadowing "f_it" Rename the first declaration to "lock_entry". --- src/goto-instrument/thread_instrumentation.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index a3a7518c2df..8c07698f891 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -120,14 +120,14 @@ void mutex_init_instrumentation(goto_modelt &goto_model) { // get pthread_mutex_lock - symbol_tablet::symbolst::const_iterator f_it= + symbol_tablet::symbolst::const_iterator lock_entry = goto_model.symbol_table.symbols.find("pthread_mutex_lock"); - if(f_it==goto_model.symbol_table.symbols.end()) + if(lock_entry == goto_model.symbol_table.symbols.end()) return; // get type of lock argument - code_typet code_type=to_code_type(to_code_type(f_it->second.type)); + code_typet code_type = to_code_type(to_code_type(lock_entry->second.type)); if(code_type.parameters().size()!=1) return; From a4c52bd2df8fb8f0d1d4fbaea6d51184882b736f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 14:00:39 +0000 Subject: [PATCH 11/14] Rename shadowing variable "i" Use target_index instead to avoid shadowing. --- src/goto-instrument/unwind.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index a7ef29eb16d..38129fd7f6e 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -55,9 +55,10 @@ void goto_unwindt::copy_segment( assert(goto_program.instructions.size()==target_vector.size()); // adjust intra-segment gotos - for(std::size_t i=0; iis_goto()) continue; From c0919920697a5bbffdc1ca6d099c6327e3374c63 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 14:25:36 +0000 Subject: [PATCH 12/14] Avoid shadowing class member "set_of_cycles" We pass different sets of cycles in there, only sometimes the actual class member itself. --- .../wmm/instrumenter_strategies.cpp | 54 ++++++++++--------- 1 file changed, 28 insertions(+), 26 deletions(-) diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp index 6acf938246e..925d9001940 100644 --- a/src/goto-instrument/wmm/instrumenter_strategies.cpp +++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp @@ -81,11 +81,12 @@ void instrumentert::instrument_with_strategy(instrumentation_strategyt strategy) } void inline instrumentert::instrument_all_inserter( - const std::set &set_of_cycles) + const std::set &subset_of_cycles) { - for(std::set::const_iterator - it=(set_of_cycles).begin(); - it!=(set_of_cycles).end(); ++it) + for(std::set::const_iterator it = + subset_of_cycles.begin(); + it != subset_of_cycles.end(); + ++it) { for(std::set::const_iterator p_it=it->unsafe_pairs.begin(); @@ -109,15 +110,16 @@ void inline instrumentert::instrument_all_inserter( } void inline instrumentert::instrument_one_event_per_cycle_inserter( - const std::set &set_of_cycles) + const std::set &subset_of_cycles) { /* to keep track of the delayed pair, and to avoid the instrumentation of two pairs in a same cycle */ std::set delayed; - for(std::set::iterator - it=set_of_cycles.begin(); - it!=set_of_cycles.end(); ++it) + for(std::set::iterator it = + subset_of_cycles.begin(); + it != subset_of_cycles.end(); + ++it) { /* cycle with already a delayed pair? */ bool next=false; @@ -189,7 +191,7 @@ unsigned inline instrumentert::cost( } void inline instrumentert::instrument_minimum_interference_inserter( - const std::set &set_of_cycles) + const std::set &subset_of_cycles) { /* Idea: We solve this by a linear programming approach, @@ -216,10 +218,10 @@ void inline instrumentert::instrument_minimum_interference_inserter( #ifdef HAVE_GLPK /* first, identify all the unsafe pairs */ std::set edges; - for(std::set::iterator - C_j=set_of_cycles.begin(); - C_j!=set_of_cycles.end(); - ++C_j) + for(std::set::iterator C_j = + subset_of_cycles.begin(); + C_j != subset_of_cycles.end(); + ++C_j) for(std::set::const_iterator e_i= C_j->unsafe_pairs.begin(); e_i!=C_j->unsafe_pairs.end(); @@ -236,8 +238,8 @@ void inline instrumentert::instrument_minimum_interference_inserter( glp_set_prob_name(lp, "instrumentation optimisation"); glp_set_obj_dir(lp, GLP_MIN); - message.debug() << "edges: "<::iterator - C_j=set_of_cycles.begin(); - C_j!=set_of_cycles.end(); - ++C_j) + for(std::set::iterator C_j = + subset_of_cycles.begin(); + C_j != subset_of_cycles.end(); + ++C_j) { ++i; std::string name="C_"+std::to_string(i); @@ -269,7 +271,7 @@ void inline instrumentert::instrument_minimum_interference_inserter( glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ } - const std::size_t mat_size=set_of_cycles.size()*edges.size(); + const std::size_t mat_size = subset_of_cycles.size() * edges.size(); message.debug() << "size of the system: " << mat_size << messaget::eom; std::vector imat(mat_size+1); @@ -287,10 +289,10 @@ void inline instrumentert::instrument_minimum_interference_inserter( ++e_i) { row=1; - for(std::set::iterator - C_j=set_of_cycles.begin(); - C_j!=set_of_cycles.end(); - ++C_j) + for(std::set::iterator C_j = + subset_of_cycles.begin(); + C_j != subset_of_cycles.end(); + ++C_j) { imat[i]=row; jmat[i]=col; @@ -344,7 +346,7 @@ void inline instrumentert::instrument_minimum_interference_inserter( glp_delete_prob(lp); #else - (void)set_of_cycles; // unused parameter + (void)subset_of_cycles; // unused parameter throw "sorry, minimum interference option requires glpk; " "please recompile goto-instrument with glpk"; #endif From e485ebab88af8664c921286eca7cf0f081b6baba Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 14:27:13 +0000 Subject: [PATCH 13/14] Do not pass in class member "ns" This avoids shadowing. --- src/goto-instrument/wmm/goto2graph.cpp | 9 ++++++--- src/goto-instrument/wmm/goto2graph.h | 13 ++++++++----- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index bd9e179ea42..22d8febc8ef 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -210,9 +210,13 @@ void instrumentert::cfg_visitort::visit_cfg_function( /* a:=b -o-> Rb -po-> Wa */ else if(instruction.is_assign()) { - visit_cfg_assign(value_sets, ns, i_it, no_dependencies + visit_cfg_assign( + value_sets, + i_it, + no_dependencies #ifdef LOCAL_MAY - , local_may + , + local_may #endif ); // NOLINT(whitespace/parens) } @@ -783,7 +787,6 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence( void instrumentert::cfg_visitort::visit_cfg_assign( value_setst &value_sets, - namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies #ifdef LOCAL_MAY diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index bf1cb30693e..89bc0e30e7c 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -125,11 +125,14 @@ class instrumentert goto_programt::const_targett i_it); void inline visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it); - void visit_cfg_assign(value_setst &value_sets, namespacet &ns, - goto_programt::instructionst::iterator &i_it, bool no_dependencies - #ifdef LOCAL_MAY - , local_may_aliast &local_may - #endif + void visit_cfg_assign( + value_setst &value_sets, + goto_programt::instructionst::iterator &i_it, + bool no_dependencies +#ifdef LOCAL_MAY + , + local_may_aliast &local_may +#endif ); // NOLINT(whitespace/parens) void visit_cfg_fence(goto_programt::instructionst::iterator i_it); void visit_cfg_skip(goto_programt::instructionst::iterator i_it); From ee34d34d7f190ccad0d419bc040f45d4155b54e5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 14:37:53 +0000 Subject: [PATCH 14/14] Do not unnecessarily pass in class member "symbol_table" Just remove the parameter. --- src/goto-instrument/wmm/shared_buffers.cpp | 1 - src/goto-instrument/wmm/shared_buffers.h | 1 - src/goto-instrument/wmm/weak_memory.cpp | 3 +-- 3 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 39964ab9841..0f140c9ed12 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -1021,7 +1021,6 @@ bool shared_bufferst::is_buffered_in_general( /// variables (non necessarily shared themselves) whose value could be changed /// as effect of a read delay void shared_bufferst::affected_by_delay( - symbol_tablet &symbol_table, value_setst &value_sets, goto_functionst &goto_functions) { diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index c9733b514fc..d80a600099f 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -184,7 +184,6 @@ class shared_bufferst goto_functionst &goto_functions); void affected_by_delay( - symbol_tablet &symbol_table, value_setst &value_sets, goto_functionst &goto_functions); diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 08ffcf7dc0a..d9014c54d3d 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -222,8 +222,7 @@ void weak_memory( shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles // for reads delays - shared_buffers.affected_by_delay( - goto_model.symbol_table, value_sets, goto_model.goto_functions); + shared_buffers.affected_by_delay(value_sets, goto_model.goto_functions); for(std::set::iterator it= shared_buffers.affected_by_delay_set.begin();