From 476270b5abfa5d0310388009766b3c3a913b3e55 Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Fri, 3 Nov 2017 16:41:44 +0000
Subject: [PATCH 1/2] catch by const ref instead of by value or non-const ref

This PR makes the update universally for std::string (where the contents of the whole string will be copied) and bad_alloc (where memory is already short).
These two are particularly prevalent.
---
 src/cbmc/bmc.cpp                                 |  6 +++---
 src/cbmc/cbmc_parse_options.cpp                  | 16 ++++++++--------
 src/clobber/clobber_parse_options.cpp            |  4 ++--
 .../goto_analyzer_parse_options.cpp              |  8 ++++----
 src/goto-cc/goto_cc_mode.cpp                     |  4 ++--
 src/goto-diff/goto_diff_parse_options.cpp        |  4 ++--
 .../accelerate/acceleration_utils.cpp            |  4 ++--
 .../disjunctive_polynomial_acceleration.cpp      |  6 +++---
 .../accelerate/polynomial_accelerator.cpp        |  8 ++++----
 .../accelerate/sat_path_enumerator.cpp           |  2 +-
 .../goto_instrument_parse_options.cpp            |  4 ++--
 src/goto-instrument/wmm/goto2graph.cpp           |  4 ++--
 src/goto-instrument/wmm/goto2graph.h             |  2 +-
 src/goto-instrument/wmm/pair_collection.cpp      |  2 +-
 src/goto-instrument/wmm/shared_buffers.cpp       |  4 ++--
 src/jbmc/jbmc_parse_options.cpp                  | 12 ++++++------
 src/memory-models/mmcc_parse_options.cpp         |  2 +-
 unit/wp.cpp                                      |  2 +-
 18 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 8a95b7cfafe..f9ede133877 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -371,7 +371,7 @@ safety_checkert::resultt bmct::run(
     return safety_checkert::resultt::ERROR;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return safety_checkert::resultt::ERROR;
@@ -471,7 +471,7 @@ safety_checkert::resultt bmct::run(
     return decide(goto_functions, prop_conv);
   }
 
-  catch(std::string &error_str)
+  catch(const std::string &error_str)
   {
     error() << error_str << eom;
     return safety_checkert::resultt::ERROR;
@@ -483,7 +483,7 @@ safety_checkert::resultt bmct::run(
     return safety_checkert::resultt::ERROR;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return safety_checkert::resultt::ERROR;
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 3b616623b9e..cccea229ada 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -435,7 +435,7 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_EXCEPTION;
   }
 
-  catch(const std::string error_msg)
+  catch(const std::string &error_msg)
   {
     error() << error_msg << eom;
     return CPROVER_EXIT_EXCEPTION;
@@ -589,7 +589,7 @@ bool cbmc_parse_optionst::set_properties()
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -649,7 +649,7 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_EXCEPTION;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return CPROVER_EXIT_EXCEPTION;
@@ -661,7 +661,7 @@ int cbmc_parse_optionst::get_goto_program(
     return CPROVER_EXIT_EXCEPTION;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
@@ -710,7 +710,7 @@ void cbmc_parse_optionst::preprocessing()
     error() << e << eom;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
   }
@@ -720,7 +720,7 @@ void cbmc_parse_optionst::preprocessing()
     error() << "Numeric exception : " << e << eom;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
@@ -844,7 +844,7 @@ bool cbmc_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -856,7 +856,7 @@ bool cbmc_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index ad6508c30e2..28768bf4567 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -153,7 +153,7 @@ int clobber_parse_optionst::doit()
     return 0;
   }
 
-  catch(const std::string error_msg)
+  catch(const std::string &error_msg)
   {
     error() << error_msg << messaget::eom;
     return 8;
@@ -165,7 +165,7 @@ int clobber_parse_optionst::doit()
     return 8;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << messaget::eom;
     return 8;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 7e388413050..536feb15c9f 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -171,7 +171,7 @@ int goto_analyzer_parse_optionst::doit()
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -340,7 +340,7 @@ bool goto_analyzer_parse_optionst::set_properties()
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -422,7 +422,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -433,7 +433,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return true;
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index f398864b6c2..b6802103f30 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -88,7 +88,7 @@ int goto_cc_modet::main(int argc, const char **argv)
     return EX_SOFTWARE;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return EX_SOFTWARE;
@@ -99,7 +99,7 @@ int goto_cc_modet::main(int argc, const char **argv)
     return EX_SOFTWARE;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return EX_SOFTWARE;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 28a2b017ed1..d439f1b9aa0 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -449,7 +449,7 @@ bool goto_diff_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -460,7 +460,7 @@ bool goto_diff_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return true;
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index 9a3ac8651f5..b6089b22aa0 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -181,7 +181,7 @@ bool acceleration_utilst::check_inductive(
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in inductiveness SAT check: " << s << '\n';
     return false;
@@ -458,7 +458,7 @@ bool acceleration_utilst::do_assumptions(
       return false;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in monotonicity SAT check: " << s << '\n';
      return false;
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index cf971a023f5..cbd10ccc48c 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -248,7 +248,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   {
     path_is_monotone=utils.do_assumptions(polynomials, path, guard);
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     // Couldn't do WP.
     std::cout << "Assumptions error: " << s << '\n';
@@ -389,7 +389,7 @@ bool disjunctive_polynomial_accelerationt::find_path(patht &path)
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
   }
@@ -637,7 +637,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
   }
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index aa4850cd401..17ab6d79ab4 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -181,7 +181,7 @@ bool polynomial_acceleratort::accelerate(
   {
     path_is_monotone=utils.do_assumptions(polynomials, loop, guard);
   }
-  catch (std::string s)
+  catch(const std::string &s)
   {
     // Couldn't do WP.
     std::cout << "Assumptions error: " << s << '\n';
@@ -424,7 +424,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
   }
@@ -485,7 +485,7 @@ bool polynomial_acceleratort::fit_const(
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
   }
@@ -719,7 +719,7 @@ bool polynomial_acceleratort::check_inductive(
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in inductiveness SAT check: " << s << '\n';
     return false;
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index b2e2177ed87..0d9c6a4eebc 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -95,7 +95,7 @@ bool sat_path_enumeratort::next(patht &path)
       return true;
     }
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
   }
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index bc6d55d960b..2218fd68235 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -763,7 +763,7 @@ int goto_instrument_parse_optionst::doit()
     return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
@@ -775,7 +775,7 @@ int goto_instrument_parse_optionst::doit()
     return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 011ef1a36ac..09afe5d1836 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -76,7 +76,7 @@ bool inline instrumentert::local(const irep_idt &id)
 
     return false;
   }
-  catch(std::string exception)
+  catch(const std::string &exception)
   {
     message.debug()<<"Exception: "<<exception << messaget::eom;
     return false;
@@ -714,7 +714,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
     cur_fun=stack_fun.pop();
     #endif
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     instrumenter.message.warning() << "sorry, doesn't handle recursion "
                                    << "(function " << fun_id << "; .cpp) "
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index c8b472e079b..ce69edc5644 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -251,7 +251,7 @@ class instrumentert
           function, empty_in, end_out);
         leave_function(function);
       }
-      catch(std::string s)
+      catch(const std::string &s)
       {
         instrumenter.message.warning() << s << messaget::eom;
       }
diff --git a/src/goto-instrument/wmm/pair_collection.cpp b/src/goto-instrument/wmm/pair_collection.cpp
index bceae75663c..d620a3bfd2f 100644
--- a/src/goto-instrument/wmm/pair_collection.cpp
+++ b/src/goto-instrument/wmm/pair_collection.cpp
@@ -53,7 +53,7 @@ void event_grapht::graph_pensieve_explorert::collect_pairs(namespacet &ns)
           first_event.source_location.get_line(), first_event.variable,
             static_cast<int>(first_event.operation));
       }
-      catch(std::string s)
+      catch(const std::string &s)
       {
         egraph.message.warning() << "failed to find" << s << messaget::eom;
         continue;
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index f68b29b2fec..741b8d01a08 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -177,7 +177,7 @@ void shared_bufferst::assignment(
 
     t++;
   }
-  catch(std::string s)
+  catch(const std::string &s)
   {
     message.warning() << s << messaget::eom;
   }
@@ -929,7 +929,7 @@ void shared_bufferst::nondet_flush(
                 buff1_thd_3_expr))))));
   }
   }
-  catch (std::string s)
+  catch(const std::string &s)
   {
     message.warning() << s << messaget::eom;
   }
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index ae7473fb8c3..7d3da461fd5 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -413,7 +413,7 @@ int jbmc_parse_optionst::doit()
     return 6; // should contemplate EX_SOFTWARE from sysexits.h
   }
 
-  catch(const std::string error_msg)
+  catch(const std::string &error_msg)
   {
     error() << error_msg << eom;
     return 6; // should contemplate EX_SOFTWARE from sysexits.h
@@ -546,7 +546,7 @@ bool jbmc_parse_optionst::set_properties()
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -605,7 +605,7 @@ int jbmc_parse_optionst::get_goto_program(
     return 6;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return 6;
@@ -616,7 +616,7 @@ int jbmc_parse_optionst::get_goto_program(
     return 6;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return 6;
@@ -769,7 +769,7 @@ bool jbmc_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(const std::string e)
+  catch(const std::string &e)
   {
     error() << e << eom;
     return true;
@@ -780,7 +780,7 @@ bool jbmc_parse_optionst::process_goto_program(
     return true;
   }
 
-  catch(std::bad_alloc)
+  catch(const std::bad_alloc &)
   {
     error() << "Out of memory" << eom;
     return true;
diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp
index 8fae9244839..03644ab95f5 100644
--- a/src/memory-models/mmcc_parse_options.cpp
+++ b/src/memory-models/mmcc_parse_options.cpp
@@ -64,7 +64,7 @@ int mmcc_parse_optionst::doit()
     std::cerr << error << '\n';
     return 10;
   }
-  catch(const std::string error)
+  catch(const std::string &error)
   {
     std::cerr << error << '\n';
     return 10;
diff --git a/unit/wp.cpp b/unit/wp.cpp
index b4f836ab7ea..04096b2977a 100644
--- a/unit/wp.cpp
+++ b/unit/wp.cpp
@@ -75,7 +75,7 @@ int main(int argc, const char **argv)
     }
   }
 
-  catch(std::string s)
+  catch(const std::string &s)
   {
     std::cerr << s << std::endl;
   }

From 7de4858dc03d94140e386aafc7644b93acfd361f Mon Sep 17 00:00:00 2001
From: Nathan Phillips <nathan.phillips@diffblue.com>
Date: Fri, 3 Nov 2017 15:12:26 +0000
Subject: [PATCH 2/2] Added copyright notice to fix linting error

---
 unit/wp.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/unit/wp.cpp b/unit/wp.cpp
index 04096b2977a..b8656120347 100644
--- a/unit/wp.cpp
+++ b/unit/wp.cpp
@@ -1,3 +1,5 @@
+// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+
 #include <iostream>
 
 #include <util/cout_message.h>