From ebbbf5f58bf6e70dd3a5c9e1aa3d0b2aa7eeee05 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Fri, 1 Sep 2017 17:01:50 +0100 Subject: [PATCH 1/5] Make goto_modelt.output const --- src/goto-programs/goto_model.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From 567eaa7cfffb4356dd9180daead5222efaf96702 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Tue, 5 Sep 2017 17:19:03 +0100 Subject: [PATCH 2/5] Make basic_blockst.output const --- src/goto-instrument/cover.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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, From 9be84eae757fb4be3d4b9b0db5a972599fd181e4 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Tue, 5 Sep 2017 17:39:11 +0100 Subject: [PATCH 3/5] Make automatont.output const --- src/goto-instrument/accelerate/trace_automaton.cpp | 2 +- src/goto-instrument/accelerate/trace_automaton.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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() { From 211fcc225eb8519d48c7efb181a125f4729fa120 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Tue, 5 Sep 2017 17:53:29 +0100 Subject: [PATCH 4/5] Make path_nodet.output const --- src/goto-instrument/accelerate/path.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From 388a25e449ce73606ac763f5fc57e5abe4b7aed7 Mon Sep 17 00:00:00 2001 From: janmroczkowski Date: Tue, 5 Sep 2017 17:58:09 +0100 Subject: [PATCH 5/5] Make uncaught_exceptions_analysis.output const --- src/analyses/uncaught_exceptions_analysis.cpp | 17 ++++++++++------- src/analyses/uncaught_exceptions_analysis.h | 2 +- 2 files changed, 11 insertions(+), 8 deletions(-) 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 &,