Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const

Make output methods const

Author: Daniel Kroening

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;
     }

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 &,

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;

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';
 

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()
   {

src/goto-instrument/cover.cpp

@@ -28,6 +28,8 @@ Date: May 2016
 #include <json/json_parser.h>
 #include <util/message.h>
 
+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,

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);