Disable nested exception printing for Windows

Due to bug in the VS2013 C++ compiler, using std::rethrow_if_nested or
std::nested_exception is not supported. This disables trying to unwrap the
exception and just prints a warning saying the nested exceptionc couldn't be
printed.

Don't use noexcept directly, pull both part of the nested exception into
a separate file to handle discrepancies.

src/goto-symex/equation_conversion_exceptions.h

@@ -40,7 +40,7 @@ class guard_conversion_exceptiont : public std::runtime_error
   {
   }
 
-  const char *what() const noexcept override
+  const char *what() const optional_noexcept override
   {
     return error_message.c_str();
   }

src/goto-symex/symex_target_equation.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "symex_target_equation.h"
 
 #include <util/std_expr.h>
+#include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
 
 #include <langapi/language_util.h>
@@ -437,7 +438,7 @@ void symex_target_equationt::convert_guards(
       }
       catch(const bitvector_conversion_exceptiont &conversion_exception)
       {
-        std::throw_with_nested(guard_conversion_exceptiont(step, ns));
+        util_throw_with_nested(guard_conversion_exceptiont(step, ns));
       }
     }
   }

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
 #include <util/std_expr.h>
+#include <util/throw_with_nested.h>
 
 #include "bv_conversion_exceptions.h"
 #include "flatten_byte_extract_exceptions.h"
@@ -51,7 +52,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     }
     catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
     {
-      std::throw_with_nested(
+      util_throw_with_nested(
         bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
     }
   }

src/solvers/flattening/flatten_byte_extract_exceptions.h

@@ -40,7 +40,7 @@ class non_const_array_sizet : public flatten_byte_extract_exceptiont
     computed_error_message = error_message.str();
   }
 
-  const char *what() const noexcept override
+  const char *what() const optional_noexcept override
   {
     return computed_error_message.c_str();
   }
@@ -73,7 +73,7 @@ class non_byte_alignedt : public flatten_byte_extract_exceptiont
     computed_error_message = error_message.str();
   }
 
-  const char *what() const noexcept override
+  const char *what() const optional_noexcept override
   {
     return computed_error_message.c_str();
   }
@@ -103,7 +103,7 @@ class non_constant_widtht : public flatten_byte_extract_exceptiont
     computed_error_message = error_message.str();
   }
 
-  const char *what() const noexcept override
+  const char *what() const optional_noexcept override
   {
     return computed_error_message.c_str();
   }
@@ -130,7 +130,7 @@ class non_const_byte_extraction_sizet : public flatten_byte_extract_exceptiont
     computed_error_message = error_message.str();
   }
 
-  const char *what() const noexcept override
+  const char *what() const optional_noexcept override
   {
     return computed_error_message.c_str();
   }

src/util/throw_with_nested.h

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: util
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_THROW_WITH_NESTED_H
+#define CPROVER_UTIL_THROW_WITH_NESTED_H
+
+#include <exception>
+
+#ifdef _MSC_VER
+#include <stdexcept>
+// TODO(tkiley): Nested exception logging not supported on windows due to a bug
+// TODO(tkiley): in MSVC++ Compiler (diffblue/cbmc#2104):
+// TODO(tkiley): https://blogs.msdn.microsoft.com/vcblog/2016/01/22/vs-2015-update-2s-stl-is-c17-so-far-feature-complete
+
+#define DISABLE_NESTED_EXCEPTIONS
+
+class non_nested_exception_support : public std::runtime_error
+{
+public:
+  non_nested_exception_support()
+    : std::runtime_error("Nested exception printing not supported on Windows")
+  {
+  }
+};
+
+#endif
+
+template <class T>
+#ifdef __GNUC__
+__attribute__((noreturn))
+#endif
+void util_throw_with_nested(T &&t)
+{
+#ifndef DISABLE_NESTED_EXCEPTIONS
+  std::throw_with_nested(t);
+#else
+  throw t;
+#endif
+}
+
+template <class E>
+void util_rethrow_if_nested(const E &e)
+{
+#ifndef DISABLE_NESTED_EXCEPTIONS
+  std::rethrow_if_nested(e);
+#else
+  // Check we've not already thrown the non_nested_support_exception
+  if(!dynamic_cast<const non_nested_exception_support *>(&e))
+  {
+    throw non_nested_exception_support();
+  }
+#endif
+}
+
+#endif // CPROVER_UTIL_THROW_WITH_NESTED_H

src/util/unwrap_nested_exception.cpp

@@ -10,6 +10,7 @@ Author: Diffblue Ltd.
 #include "invariant.h"
 #include "string_utils.h"
 #include "suffix.h"
+#include "throw_with_nested.h"
 
 #include <sstream>
 #include <vector>
@@ -32,7 +33,7 @@ std::string unwrap_exception(const std::exception &e, int level)
 
   try
   {
-    std::rethrow_if_nested(e);
+    util_rethrow_if_nested(e);
   }
   catch(const std::exception &e)
   {