diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 65baa49e082..4b0674c375d 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -186,19 +186,22 @@ void uncaught_exceptions_analysist::collect_uncaught_exceptions( /// Prints the exceptions map that maps each method to the set of exceptions /// that may escape it void uncaught_exceptions_analysist::output( - const goto_functionst &goto_functions) + const goto_functionst &goto_functions) const { #ifdef DEBUG forall_goto_functions(it, goto_functions) { - if(exceptions_map[it->first].size()>0) + const auto fn=it->first; + const exceptions_mapt::const_iterator found=exceptions_map.find(fn); + INVARIANT( + found!=exceptions_map.end(), + "each function expected to be recorded in `exceptions_map`"); + const auto &fs=found->second; + if(!fs.empty()) { std::cout << "Uncaught exceptions in function " << - it->first << ": " << std::endl; - INVARIANT( - exceptions_map.find(it->first)!=exceptions_map.end(), - "each function expected to be recorded in `exceptions_map`"); - for(auto exc_id : exceptions_map[it->first]) + fn << ": " << std::endl; + for(const auto exc_id : fs) std::cout << id2string(exc_id) << " "; std::cout << std::endl; } diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h index a53998b4bd2..aef256afba0 100644 --- a/src/analyses/uncaught_exceptions_analysis.h +++ b/src/analyses/uncaught_exceptions_analysis.h @@ -64,7 +64,7 @@ class uncaught_exceptions_analysist const goto_functionst &, const namespacet &); - void output(const goto_functionst &); + void output(const goto_functionst &) const; void operator()( const goto_functionst &, diff --git a/src/goto-instrument/accelerate/path.h b/src/goto-instrument/accelerate/path.h index 7dae7fcf989..9044e0e3f72 100644 --- a/src/goto-instrument/accelerate/path.h +++ b/src/goto-instrument/accelerate/path.h @@ -36,7 +36,7 @@ class path_nodet { } - void output(const goto_programt &program, std::ostream &str); + void output(const goto_programt &program, std::ostream &str) const; goto_programt::targett loc; const exprt guard; diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 551d0c7b6d8..6a070807553 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -473,7 +473,7 @@ void trace_automatont::minimise() determinise(); } -void automatont::output(std::ostream &str) +void automatont::output(std::ostream &str) const { str << "Init: " << init_state << '\n'; diff --git a/src/goto-instrument/accelerate/trace_automaton.h b/src/goto-instrument/accelerate/trace_automaton.h index cb113ef1076..b4d31159175 100644 --- a/src/goto-instrument/accelerate/trace_automaton.h +++ b/src/goto-instrument/accelerate/trace_automaton.h @@ -54,7 +54,7 @@ class automatont std::size_t count_transitions(); - void output(std::ostream &str); + void output(std::ostream &str) const; void clear() { diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 258b790a887..d76afe03b71 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -28,6 +28,8 @@ Date: May 2016 #include #include +namespace +{ class basic_blockst { public: @@ -237,7 +239,7 @@ class basic_blockst } } - void output(std::ostream &out) + void output(std::ostream &out) const { for(block_mapt::const_iterator b_it=block_map.begin(); @@ -289,6 +291,7 @@ class basic_blockst block_info.source_location.set_basic_block_covered_lines(covered_lines); } }; +} bool coverage_goalst::get_coverage_goals( const std::string &coverage_file, diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 6e9ebbc6f37..2f9c5939bc2 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -31,7 +31,7 @@ class goto_modelt goto_functions.clear(); } - void output(std::ostream &out) + void output(std::ostream &out) const { namespacet ns(symbol_table); goto_functions.output(ns, out);