Silence spurious/information-only Visual Studio warnings [blocks: #2310]

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -436,11 +436,19 @@ bool java_bytecode_parsert::parse()
     return true;
   }
 
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     error() << "parsing error" << eom;
     return true;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   return false;
 }

src/goto-analyzer/taint_analysis.cpp

@@ -402,11 +402,19 @@ bool taint_analysist::operator()(
     error() << error_msg << eom;
     return true;
   }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     error() << "Caught unexpected error in taint_analysist::operator()" << eom;
     return true;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 }
 
 bool taint_analysis(

src/goto-cc/ms_cl_cmdline.h

@@ -32,6 +32,8 @@ class ms_cl_cmdlinet:public goto_cc_cmdlinet
   void process_cl_option(const std::string &s);
   void process_response_file(const std::string &file);
   void process_response_file_line(const std::string &line);
+  // avoid spurious warning about overloading
+  using cmdlinet::parse;
   bool parse(const std::vector<std::string> &);
 };
 

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -870,10 +870,18 @@ bool acceleration_utilst::expr2poly(
   {
     poly.from_expr(subbed_expr);
   }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     return false;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   return true;
 }
@@ -1094,6 +1102,11 @@ bool acceleration_utilst::assign_array(
       poly.from_expr(idx);
     }
   }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     // idx is probably nonlinear... bail out.
@@ -1102,6 +1115,9 @@ bool acceleration_utilst::assign_array(
 #endif
     return false;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   if(poly.max_degree(loop_counter) > 1)
   {

src/goto-instrument/wmm/shared_buffers.cpp

@@ -1249,11 +1249,19 @@ void shared_bufferst::cfg_visitort::weak_memory(
 
         i_it--; // the for loop already counts us up
       }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
       catch (...)
       {
         shared_buffers.message.warning() << "Identifier not found"
           << messaget::eom;
       }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
     }
     else if(is_fence(instruction, ns) ||
             (instruction.is_other() &&

src/goto-programs/cfg.h

@@ -188,6 +188,11 @@ class concurrent_cfg_baset:public virtual cfg_baset<T, P, I>
     typename cfg_baset<T, P, I>::entryt &entry);
 };
 
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable:4435)
+  // object layout under /vd2 will change due to virtual base class
+#endif
 template<class T,
          typename P=const goto_programt,
          typename I=goto_programt::const_targett>
@@ -201,6 +206,7 @@ class procedure_local_cfg_baset:public virtual cfg_baset<T, P, I>
     goto_programt::const_targett next_PC,
     typename cfg_baset<T, P, I>::entryt &entry);
 };
+#include <util/pragma_pop.def>
 
 template<class T,
          typename P=const goto_programt,

src/goto-programs/read_goto_binary.cpp

@@ -167,10 +167,18 @@ bool is_goto_binary(const std::string &filename)
         return true;
     }
 
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
     catch(...)
     {
       // ignore any errors
     }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   }
   else if(is_osx_fat_magic(hdr))
   {
@@ -183,10 +191,18 @@ bool is_goto_binary(const std::string &filename)
         return true;
     }
 
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
     catch(...)
     {
       // ignore any errors
     }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   }
 
   return false;
@@ -216,10 +232,18 @@ bool read_object_and_link(
   {
     link_goto_model(dest, temp_model, message_handler);
   }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     return true;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   // reading successful, let's update config
   config.set_from_symbol_table(dest.symbol_table);

src/linking/static_lifetime_init.cpp

@@ -123,10 +123,18 @@ bool static_lifetime_init(
         rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
         assert(rhs.is_not_nil());
       }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
       catch(...)
       {
         return true;
       }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
     }
     else
       rhs=symbol.value;

src/util/simplify_utils.cpp

@@ -46,6 +46,12 @@ bool sort_operands(exprt::operandst &operands)
 // aren't associative. Addition to pointers isn't really
 // associative.
 
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable:4510)
+#pragma warning(disable:4610)
+  // default constructor could not be generated
+#endif
 struct saj_tablet
 {
   const irep_idt id;
@@ -93,6 +99,7 @@ struct saj_tablet
                irep_idt()  }},
   { irep_idt(), { irep_idt() }}
 };
+#include <util/pragma_pop.def>
 
 static bool sort_and_join(
   const struct saj_tablet &saj_entry,

src/util/symbol_table.cpp

@@ -20,6 +20,11 @@ std::pair<symbolt &, bool> symbol_tablet::insert(symbolt symbol)
   symbolt &new_symbol=result.first->second;
   if(result.second)
   {
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
     try
     {
       symbol_base_mapt::iterator base_result=
@@ -39,6 +44,7 @@ std::pair<symbolt &, bool> symbol_tablet::insert(symbolt symbol)
       internal_symbols.erase(result.first);
       throw;
     }
+#include <util/pragma_pop.def>
   }
   return std::make_pair(std::ref(new_symbol), result.second);
 }

src/util/unwrap_nested_exception.cpp

@@ -46,9 +46,17 @@ std::string unwrap_exception(const std::exception &e, int level)
     }
     message_stream << nested_message;
   }
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4571)
+  // catch(...) semantics changed since Visual C++ 7.1
+#endif
   catch(...)
   {
     UNREACHABLE;
   }
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   return message_stream.str();
 }