Silence Visual Studio warnings about non-thread-safe static objects

Author: tautschnig

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -65,7 +65,15 @@ ci_lazy_methodst::ci_lazy_methodst(
 ///   class
 static bool references_class_model(const exprt &expr)
 {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
   static const struct_tag_typet class_type("java::java.lang.Class");
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
   {

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -89,9 +89,17 @@ static bool should_init_symbol(const symbolt &sym)
 /// \return Class initializer method's symbol name.
 irep_idt get_java_class_literal_initializer_signature()
 {
-  static irep_idt signature =
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
+  static const irep_idt signature =
     "java::java.lang.Class.cproverInitializeClassLiteral:"
     "(Ljava/lang/String;ZZZZZZZ)V";
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   return signature;
 }
 

jbmc/src/java_bytecode/java_utils.cpp

@@ -407,9 +407,17 @@ get_inherited_component(
 /// \return true if this static field is known never to be null
 bool is_non_null_library_global(const irep_idt &symbolid)
 {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
   static const irep_idt in = "java::java.lang.System.in";
   static const irep_idt out = "java::java.lang.System.out";
   static const irep_idt err = "java::java.lang.System.err";
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   return symbolid == in || symbolid == out || symbolid == err;
 }
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1049,7 +1049,15 @@ bool jbmc_parse_optionst::process_goto_functions(
 
 bool jbmc_parse_optionst::can_generate_function_body(const irep_idt &name)
 {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
   static const irep_idt initialize_id = INITIALIZE_FUNCTION;
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   return name != goto_functionst::entry_point() && name != initialize_id;
 }

src/analyses/reaching_definitions.cpp

@@ -734,7 +734,15 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get(
 {
   populate_cache(identifier);
 
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
   static ranges_at_loct empty;
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
   export_cachet::const_iterator entry=export_cache.find(identifier);
 

src/goto-instrument/wmm/event_graph.h

@@ -349,7 +349,15 @@ class event_grapht
 
     std::list<event_idt>* initial_filtering(std::list<event_idt>* order)
     {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
       static std::list<event_idt> new_order;
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
 
       /* intersection */
       for(const auto &evt : *order)

src/solvers/sat/satcheck_minisat2.cpp

@@ -20,8 +20,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/threeval.h>
 
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
 #include <minisat/core/Solver.h>
 #include <minisat/simp/SimpSolver.h>
+#include <util/pragma_pop.def>
 
 #ifndef HAVE_MINISAT2
 #error "Expected HAVE_MINISAT2"

src/util/irep.cpp

@@ -209,15 +209,33 @@ const irep_idt &irept::get(const irep_namet &name) const
   if(it==s.end() ||
      it->first!=name)
   {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
     static const irep_idt empty;
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
     return empty;
   }
 #else
   named_subt::const_iterator it=s.find(name);
 
   if(it==s.end())
   {
+#ifdef _MSC_VER
+// NOLINTNEXTLINE(build/include)
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
     static const irep_idt empty;
+#ifdef _MSC_VER
+// NOLINTNEXTLINE(build/include)
+#include <util/pragma_pop.def>
+#endif
     return empty;
   }
 #endif

src/util/string_container.h

@@ -92,7 +92,15 @@ class string_containert
 /// Get a reference to the global string container.
 inline string_containert &get_string_container()
 {
+#ifdef _MSC_VER
+#include <util/pragma_push.def>
+#pragma warning(disable:4640)
+  // construction of local static object is not thread-safe
+#endif
   static string_containert ret;
+#ifdef _MSC_VER
+#include <util/pragma_pop.def>
+#endif
   return ret;
 }