Use non-truncating cast of constant expressions

Author: tautschnig

src/ansi-c/c_preprocess.cpp

@@ -325,7 +325,8 @@ bool c_preprocess_visual_studio(
 
     // This marks the command file as UTF-8, which Visual Studio
     // understands.
-    command_file << char(0xef) << char(0xbb) << char(0xbf);
+    command_file << (unsigned char)0xefu << (unsigned char)0xbbu
+                 << (unsigned char)0xbfu;
 
     command_file << "/nologo" << '\n';
     command_file << "/E" << '\n';

src/goto-cc/ms_cl_cmdline.cpp

@@ -180,9 +180,9 @@ void ms_cl_cmdlinet::process_response_file(const std::string &file)
   // these may be Unicode -- which is indicated by 0xff 0xfe
   std::string line;
   getline(infile, line);
-  if(line.size()>=2 &&
-     line[0]==static_cast<char>(0xff) &&
-     line[1]==static_cast<char>(0xfe))
+  if(
+    line.size() >= 2 && static_cast<unsigned char>(line[0]) == 0xffu &&
+    static_cast<unsigned char>(line[1]) == 0xfeu)
   {
     // Unicode, UTF-16 little endian
 
@@ -206,10 +206,10 @@ void ms_cl_cmdlinet::process_response_file(const std::string &file)
 
     #endif
   }
-  else if(line.size()>=3 &&
-          line[0]==static_cast<char>(0xef) &&
-          line[1]==static_cast<char>(0xbb) &&
-          line[2]==static_cast<char>(0xbf))
+  else if(
+    line.size() >= 3 && static_cast<unsigned char>(line[0]) == 0xefu &&
+    static_cast<unsigned char>(line[1]) == 0xbbu &&
+    static_cast<unsigned char>(line[2]) == 0xbfu)
   {
     // This is the UTF-8 BOM. We can proceed as usual, since
     // we use UTF-8 internally.

src/goto-cc/ms_link_cmdline.cpp

@@ -124,8 +124,8 @@ void ms_link_cmdlinet::process_response_file(const std::string &file)
   std::string line;
   getline(infile, line);
   if(
-    line.size() >= 2 && line[0] == static_cast<char>(0xff) &&
-    line[1] == static_cast<char>(0xfe))
+    line.size() >= 2 && static_cast<unsigned char>(line[0]) == 0xffu &&
+    static_cast<unsigned char>(line[1]) == 0xfeu)
   {
     // Unicode, UTF-16 little endian
 
@@ -150,8 +150,9 @@ void ms_link_cmdlinet::process_response_file(const std::string &file)
 #endif
   }
   else if(
-    line.size() >= 3 && line[0] == static_cast<char>(0xef) &&
-    line[1] == static_cast<char>(0xbb) && line[2] == static_cast<char>(0xbf))
+    line.size() >= 3 && static_cast<unsigned char>(line[0]) == 0xefu &&
+    static_cast<unsigned char>(line[1]) == 0xbbu &&
+    static_cast<unsigned char>(line[2]) == 0xbfu)
   {
     // This is the UTF-8 BOM. We can proceed as usual, since
     // we use UTF-8 internally.

src/solvers/smt2/smt2_tokenizer.cpp

@@ -225,7 +225,13 @@ void smt2_tokenizert::get_token_from_stream()
     case ' ':
     case '\r':
     case '\t':
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable : 4309)
+      // truncation of constant value
+#endif
     case static_cast<char>(160): // non-breaking space
+#include <util/pragma_pop.def>
       // skip any whitespace
       break;
 

src/util/config.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "config.h"
 
 #include <cstdlib>
+#include <limits>
 
 #include "arith_tools.h"
 #include "cmdline.h"
@@ -1001,16 +1002,22 @@ bool configt::set(const cmdlinet &cmdline)
     INVARIANT(
       ansi_c.double_width == sizeof(double) * 8,
       "double width shall be equal to the system double width");
+#include <util/pragma_push.def>
+#ifdef _MSC_VER
+#pragma warning(disable : 4309)
+// truncation of constant value
+#endif
     INVARIANT(
       ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
       "char_is_unsigned flag shall indicate system char unsignedness");
+#include <util/pragma_pop.def>
 
-    #ifndef _WIN32
+#ifndef _WIN32
     // On Windows, long double width varies by compiler
     INVARIANT(
       ansi_c.long_double_width == sizeof(long double) * 8,
       "long double width shall be equal to the system long double width");
-    #endif
+#endif
   }
 
   // the following allows overriding the defaults