From 13b77d843e7d6e5726bc7a9f679e7e166ffcbd3a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Feb 2018 09:05:09 +0000 Subject: [PATCH] Include list where using a std::list and drop forall_expr_list macro expr_listt was a rarely used global typedef with corresponding forall_expr_list helper macros. Instead, declare the type locally where used and use a ranged for. This avoids bringing the include to all files (transitively) including expr.h. --- src/analyses/uninitialized_domain.cpp | 8 ++++++-- src/ansi-c/ansi_c_parse_tree.h | 2 ++ src/ansi-c/c_typecast.h | 2 ++ src/ansi-c/printf_formatter.h | 2 ++ src/cbmc/bmc.cpp | 4 ++-- src/cbmc/bmc.h | 2 +- src/cpp/cpp_parse_tree.h | 2 ++ src/cpp/cpp_token_buffer.h | 2 ++ .../accelerate/acceleration_utils.h | 2 ++ src/goto-instrument/uninitialized.cpp | 20 +++++++++---------- src/goto-programs/goto_convert.cpp | 9 ++++----- src/goto-programs/goto_program.cpp | 8 ++++---- src/goto-programs/goto_program_template.h | 1 + src/goto-symex/slice.cpp | 11 +++++----- src/goto-symex/slice.h | 7 +++++-- src/goto-symex/symex_slice_class.h | 3 +-- src/pointer-analysis/add_failed_symbols.cpp | 2 ++ src/pointer-analysis/value_set_fi.h | 1 + src/util/expr.h | 10 ---------- src/util/std_code.h | 1 + 20 files changed, 56 insertions(+), 43 deletions(-) diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 4f92eaebd49..5cff1d3f0b9 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -16,6 +16,8 @@ Date: January 2010 #include #include +#include + void uninitialized_domaint::transform( locationt from, locationt to, @@ -43,10 +45,12 @@ void uninitialized_domaint::transform( std::list read=expressions_read(*from); std::list written=expressions_written(*from); - forall_expr_list(it, written) assign(*it); + for(const auto &expr : written) + assign(expr); // we only care about the *first* uninitalized use - forall_expr_list(it, read) assign(*it); + for(const auto &expr : read) + assign(expr); } } } diff --git a/src/ansi-c/ansi_c_parse_tree.h b/src/ansi-c/ansi_c_parse_tree.h index c346b5853fe..663d60fa239 100644 --- a/src/ansi-c/ansi_c_parse_tree.h +++ b/src/ansi-c/ansi_c_parse_tree.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_declaration.h" +#include + class ansi_c_parse_treet { public: diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h index efd95f998b6..11e379f3935 100644 --- a/src/ansi-c/c_typecast.h +++ b/src/ansi-c/c_typecast.h @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + // try a type cast from expr.type() to type // // false: typecast successful, expr modified diff --git a/src/ansi-c/printf_formatter.h b/src/ansi-c/printf_formatter.h index 0e48ac60e2a..1f934353a55 100644 --- a/src/ansi-c/printf_formatter.h +++ b/src/ansi-c/printf_formatter.h @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + class printf_formattert { public: diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 71d096b25bb..9bc86d3eec6 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -139,8 +139,8 @@ void bmct::do_conversion() { status() << "converting constraints" << eom; - forall_expr_list(it, bmc_constraints) - prop_conv.set_to_true(*it); + for(const auto &constraint : bmc_constraints) + prop_conv.set_to_true(constraint); } // hook for cegis to freeze synthesis program vars freeze_program_variables(); diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 6a0f7297a18..b3f9a7846e1 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -60,7 +60,7 @@ class bmct:public safety_checkert virtual ~bmct() { } // additional stuff - expr_listt bmc_constraints; + std::list bmc_constraints; void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } diff --git a/src/cpp/cpp_parse_tree.h b/src/cpp/cpp_parse_tree.h index afcd706fcef..a341f2cfa81 100644 --- a/src/cpp/cpp_parse_tree.h +++ b/src/cpp/cpp_parse_tree.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_item.h" +#include + class cpp_parse_treet { public: diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h index 859945787bd..b24f84dbe70 100644 --- a/src/cpp/cpp_token_buffer.h +++ b/src/cpp/cpp_token_buffer.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_token.h" +#include + class cpp_token_buffert { public: diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index 8d9046768ee..3d12c7db549 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -12,6 +12,7 @@ Author: Matt Lewis #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H +#include #include #include @@ -30,6 +31,7 @@ Author: Matt Lewis #include "cone_of_influence.h" typedef std::unordered_map expr_mapt; +typedef std::list expr_listt; class acceleration_utilst { diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 188e750b2c9..e01493a0f22 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -47,17 +47,17 @@ void uninitializedt::get_tracking(goto_programt::const_targett i_it) { std::list objects=objects_read(*i_it); - forall_expr_list(o_it, objects) + for(const auto &object : objects) { - if(o_it->id()==ID_symbol) + if(object.id() == ID_symbol) { - const irep_idt &identifier=to_symbol_expr(*o_it).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).get_identifier(); const std::set &uninitialized= uninitialized_analysis[i_it].uninitialized; if(uninitialized.find(identifier)!=uninitialized.end()) tracking.insert(identifier); } - else if(o_it->id()==ID_dereference) + else if(object.id() == ID_dereference) { } } @@ -142,11 +142,11 @@ void uninitializedt::add_assertions(goto_programt &goto_program) uninitialized_analysis[i_it].uninitialized; // check tracking variables - forall_expr_list(it, read) + for(const auto &object : read) { - if(it->id()==ID_symbol) + if(object.id() == ID_symbol) { - const irep_idt &identifier=to_symbol_expr(*it).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).get_identifier(); if(uninitialized.find(identifier)!=uninitialized.end()) { @@ -169,11 +169,11 @@ void uninitializedt::add_assertions(goto_programt &goto_program) } // set tracking variables - forall_expr_list(it, written) + for(const auto &object : written) { - if(it->id()==ID_symbol) + if(object.id() == ID_symbol) { - const irep_idt &identifier=to_symbol_expr(*it).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).get_identifier(); if(tracking.find(identifier)!=tracking.end()) { diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 899e4cd7d33..bcc1328c078 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1898,9 +1898,9 @@ void goto_convertt::generate_conditional_branch( std::list op; collect_operands(guard, guard.id(), op); - forall_expr_list(it, op) + for(const auto &expr : op) generate_conditional_branch( - boolean_negate(*it), target_false, source_location, dest); + boolean_negate(expr), target_false, source_location, dest); goto_programt::targett t_true=dest.add_instruction(); t_true->make_goto(target_true); @@ -1921,9 +1921,8 @@ void goto_convertt::generate_conditional_branch( std::list op; collect_operands(guard, guard.id(), op); - forall_expr_list(it, op) - generate_conditional_branch( - *it, target_true, source_location, dest); + for(const auto &expr : op) + generate_conditional_branch(expr, target_true, source_location, dest); goto_programt::targett t_false=dest.add_instruction(); t_false->make_goto(target_false); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 9b194fc4e5b..00e7a5ff49d 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -358,8 +358,8 @@ std::list objects_read( std::list dest; - forall_expr_list(it, expressions) - objects_read(*it, dest); + for(const auto &expr : expressions) + objects_read(expr, dest); return dest; } @@ -385,8 +385,8 @@ std::list objects_written( std::list dest; - forall_expr_list(it, expressions) - objects_written(*it, dest); + for(const auto &expr : expressions) + objects_written(expr, dest); return dest; } diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 2727e628054..852e380bc4a 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index 67795005c37..654c45bbb68 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -33,11 +33,11 @@ void symex_slicet::get_symbols(const typet &type) void symex_slicet::slice( symex_target_equationt &equation, - const expr_listt &exprs) + const std::list &exprs) { // collect dependencies - forall_expr_list(expr_it, exprs) - get_symbols(*expr_it); + for(const auto &expr : exprs) + get_symbols(expr); slice(equation); } @@ -229,8 +229,9 @@ void collect_open_variables( /// \param equation: symex trace to be sliced /// \param expression: list of expressions, targets for slicing /// \return None. But equation is modified as a side-effect. -void slice(symex_target_equationt &equation, - const expr_listt &expressions) +void slice( + symex_target_equationt &equation, + const std::list &expressions) { symex_slicet symex_slice; symex_slice.slice(equation, expressions); diff --git a/src/goto-symex/slice.h b/src/goto-symex/slice.h index 2bc887a0c9f..ca1111ea648 100644 --- a/src/goto-symex/slice.h +++ b/src/goto-symex/slice.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" +#include + // slice an equation with respect to the assertions contained therein void slice(symex_target_equationt &equation); @@ -21,8 +23,9 @@ void slice(symex_target_equationt &equation); void simple_slice(symex_target_equationt &equation); // Slice the symex trace with respect to a list of given expressions -void slice(symex_target_equationt &equation, - const expr_listt &expressions); +void slice( + symex_target_equationt &equation, + const std::list &expressions); // Collects "open" variables that are used but not assigned diff --git a/src/goto-symex/symex_slice_class.h b/src/goto-symex/symex_slice_class.h index 413a0bdc472..30fc4766f40 100644 --- a/src/goto-symex/symex_slice_class.h +++ b/src/goto-symex/symex_slice_class.h @@ -20,8 +20,7 @@ class symex_slicet public: void slice(symex_target_equationt &equation); - void slice(symex_target_equationt &equation, - const expr_listt &expressions); + void slice(symex_target_equationt &, const std::list &); void collect_open_variables( const symex_target_equationt &equation, diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index fe64957bf29..9969dd360cc 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + /// Get the name of the special symbol used to denote an unknown referee pointed /// to by a given pointer-typed symbol. /// \param id: base symbol id diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 4eee62763ac..2e1c1699b97 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H +#include #include #include #include diff --git a/src/util/expr.h b/src/util/expr.h index b58803f5689..aadbf671816 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -33,14 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com for(exprt::operandst::iterator it=(expr).begin(); \ it!=(expr).end(); ++it) -#define forall_expr_list(it, expr) \ - for(expr_listt::const_iterator it=(expr).begin(); \ - it!=(expr).end(); ++it) - -#define Forall_expr_list(it, expr) \ - for(expr_listt::iterator it=(expr).begin(); \ - it!=(expr).end(); ++it) - class depth_iteratort; class const_depth_iteratort; class const_unique_depth_iteratort; @@ -178,8 +170,6 @@ class exprt:public irept const_unique_depth_iteratort unique_depth_cend() const; }; -typedef std::list expr_listt; - class expr_visitort { public: diff --git a/src/util/std_code.h b/src/util/std_code.h index e5b1c1b9a49..768e4b545a7 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_STD_CODE_H #include +#include #include "expr.h" #include "expr_cast.h"