From f71661749315cdd94a8d18e7ec32cdcba0c35226 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Jul 2018 10:30:01 +0100 Subject: [PATCH] Silence spurious/information-only Visual Studio warnings --- .../java_bytecode/java_bytecode_parser.cpp | 8 +++++++ src/goto-analyzer/taint_analysis.cpp | 8 +++++++ src/goto-cc/ms_cl_cmdline.h | 2 ++ .../accelerate/acceleration_utils.cpp | 16 +++++++++++++ src/goto-instrument/wmm/shared_buffers.cpp | 8 +++++++ src/goto-programs/cfg.h | 6 +++++ src/goto-programs/read_goto_binary.cpp | 24 +++++++++++++++++++ src/linking/static_lifetime_init.cpp | 8 +++++++ src/util/simplify_utils.cpp | 7 ++++++ src/util/symbol_table.cpp | 6 +++++ src/util/unwrap_nested_exception.cpp | 8 +++++++ 11 files changed, 101 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index ef41a7366f4..8dda904cf2d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -436,11 +436,19 @@ bool java_bytecode_parsert::parse() return true; } +#ifdef _MSC_VER +#include +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { error() << "parsing error" << eom; return true; } +#ifdef _MSC_VER +#include +#endif return false; } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 67539387227..c212ede801a 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -402,11 +402,19 @@ bool taint_analysist::operator()( error() << error_msg << eom; return true; } +#ifdef _MSC_VER +#include +#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 +#endif } bool taint_analysis( diff --git a/src/goto-cc/ms_cl_cmdline.h b/src/goto-cc/ms_cl_cmdline.h index 0c05f1e7577..7841913e409 100644 --- a/src/goto-cc/ms_cl_cmdline.h +++ b/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 &); }; diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index a04c5ef1a22..0e4a05b07bd 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -870,10 +870,18 @@ bool acceleration_utilst::expr2poly( { poly.from_expr(subbed_expr); } +#ifdef _MSC_VER +#include +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { return false; } +#ifdef _MSC_VER +#include +#endif return true; } @@ -1094,6 +1102,11 @@ bool acceleration_utilst::assign_array( poly.from_expr(idx); } } +#ifdef _MSC_VER +#include +#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 +#endif if(poly.max_degree(loop_counter) > 1) { diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 2f0ab8d23cf..ecd7029287a 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/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 +#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 +#endif } else if(is_fence(instruction, ns) || (instruction.is_other() && diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index ee77dd6ce37..623134faeda 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -188,6 +188,11 @@ class concurrent_cfg_baset:public virtual cfg_baset typename cfg_baset::entryt &entry); }; +#include +#ifdef _MSC_VER +#pragma warning(disable:4435) + // object layout under /vd2 will change due to virtual base class +#endif template @@ -201,6 +206,7 @@ class procedure_local_cfg_baset:public virtual cfg_baset goto_programt::const_targett next_PC, typename cfg_baset::entryt &entry); }; +#include template +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { // ignore any errors } +#ifdef _MSC_VER +#include +#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 +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { // ignore any errors } +#ifdef _MSC_VER +#include +#endif } return false; @@ -216,10 +232,18 @@ bool read_object_and_link( { link_goto_model(dest, temp_model, message_handler); } +#ifdef _MSC_VER +#include +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { return true; } +#ifdef _MSC_VER +#include +#endif // reading successful, let's update config config.set_from_symbol_table(dest.symbol_table); diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index f27374eba53..773e5505b03 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/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 +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { return true; } +#ifdef _MSC_VER +#include +#endif } else rhs=symbol.value; diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 53b2f38f7e1..98a99bfbb57 100644 --- a/src/util/simplify_utils.cpp +++ b/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 +#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 static bool sort_and_join( const struct saj_tablet &saj_entry, diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 6557feb5c14..8b5ccf30143 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -20,6 +20,11 @@ std::pair symbol_tablet::insert(symbolt symbol) symbolt &new_symbol=result.first->second; if(result.second) { +#include +#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 symbol_tablet::insert(symbolt symbol) internal_symbols.erase(result.first); throw; } +#include } return std::make_pair(std::ref(new_symbol), result.second); } diff --git a/src/util/unwrap_nested_exception.cpp b/src/util/unwrap_nested_exception.cpp index 0689391466b..ac93f4e7a46 100644 --- a/src/util/unwrap_nested_exception.cpp +++ b/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 +#pragma warning(disable:4571) + // catch(...) semantics changed since Visual C++ 7.1 +#endif catch(...) { UNREACHABLE; } +#ifdef _MSC_VER +#include +#endif return message_stream.str(); }