Merge pull request #2292 from tautschnig/c++-windows

C++ regression tests on Windows

Author: tautschnig

appveyor.yml

@@ -86,19 +86,6 @@ test_script:
     rmdir /s /q cbmc\byte_update7
     rmdir /s /q cbmc\pipe1
     rmdir /s /q cbmc\unsigned___int128
-    rmdir /s /q cbmc-cpp
-    rmdir /s /q cpp\Decltype1
-    rmdir /s /q cpp\Decltype2
-    rmdir /s /q cpp\Function_Overloading1
-    rmdir /s /q cpp\Resolver10
-    rmdir /s /q cpp\Resolver11
-    rmdir /s /q cpp\Template_Parameters1
-    rmdir /s /q cpp\enum2
-    rmdir /s /q cpp\enum7
-    rmdir /s /q cpp\enum8
-    rmdir /s /q cpp\nullptr1
-    rmdir /s /q cpp\sizeof1
-    rmdir /s /q cpp\static_assert1
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
     cd ..

regression/cpp/Constant2/main.cpp

@@ -1,10 +1,8 @@
-#include <cassert>
-
 int const C=10;
 
 int main()
 {
-  assert(C==10);
+  __CPROVER_assert(C == 10, "");
 
   // this is *not* allowed
   ((int &)C)=20;

regression/cpp/Function_Overloading1/main.cpp

@@ -1,17 +1,23 @@
+#ifdef __GNUC__
+#define NOTHROW __attribute__((nothrow))
+#else
+#define NOTHROW
+#endif
+
 namespace std {
   // cmath
-  __inline float abs(float x) __attribute__((nothrow));
-  __inline double abs(double x) __attribute__((nothrow));
-  __inline long double abs(long double x) __attribute__((nothrow));
+  __inline float abs(float x) NOTHROW;
+  __inline double abs(double x) NOTHROW;
+  __inline long double abs(long double x) NOTHROW;
 }
 
 namespace std {
   extern "C" {
-    int abs(int) __attribute__((nothrow)) ;
+    int abs(int) NOTHROW ;
   }
   extern "C++" {
-    inline long abs(long n) __attribute__((nothrow));
-    inline long long abs(long long n) __attribute__((nothrow));
+    inline long abs(long n) NOTHROW;
+    inline long long abs(long long n) NOTHROW;
   }
 }
 

regression/cpp/Resolver10/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 struct A
 {
   int i;

regression/cpp/Resolver11/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 struct A
 {
   bool func() { return false; }

regression/cpp/Template_Parameters1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 // V depends on Ty
 template<typename Ty, Ty V>
 class T

regression/cpp/enum7/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$

regression/cpp/enum8/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 enum E1 { e1 } e1_var;
 enum E2 { e2 } e2_var;
 
@@ -23,19 +21,19 @@ struct some_struct
 
 int main()
 {
-  assert(f(0)==0);
-  assert(f(e1)==1);
-  assert(f(e2)==2);
-  assert(f(e1_var)==1);
-  assert(f(e2_var)==2);
-
-  assert(g(0)==0);
-  assert(g(e1)==1);
-  assert(g(e2)==0);
-  assert(g(e1_var)==1);
-  assert(g(e2_var)==0);
-
-  assert(f(some_struct_var.i)==0);
-  assert(f(some_struct_var.e1)==1);
-  assert(f(some_struct_var.e2)==2);
+  __CPROVER_assert(f(0) == 0, "");
+  __CPROVER_assert(f(e1) == 1, "");
+  __CPROVER_assert(f(e2) == 2, "");
+  __CPROVER_assert(f(e1_var) == 1, "");
+  __CPROVER_assert(f(e2_var) == 2, "");
+
+  __CPROVER_assert(g(0) == 0, "");
+  __CPROVER_assert(g(e1) == 1, "");
+  __CPROVER_assert(g(e2) == 0, "");
+  __CPROVER_assert(g(e1_var) == 1, "");
+  __CPROVER_assert(g(e2_var) == 0, "");
+
+  __CPROVER_assert(f(some_struct_var.i) == 0, "");
+  __CPROVER_assert(f(some_struct_var.e1) == 1, "");
+  __CPROVER_assert(f(some_struct_var.e2) == 2, "");
 }

regression/cpp/nullptr1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 typedef decltype(nullptr) nullptr_t;
 
 static_assert(nullptr==0, "nullptr==0");
@@ -20,7 +18,7 @@ int main()
 
   char buffer[10];
   void *p=my_null, *q=buffer;
-  assert(q!=nullptr);
+  __CPROVER_assert(q != nullptr, "");
 
   something(nullptr);
 }

src/goto-cc/ms_cl_cmdline.cpp

@@ -406,6 +406,7 @@ const char *ms_cl_prefixes[]=
   "MT", //  link with LIBCMT.LIB
   "MDd", //  link with MSVCRTD.LIB debug lib
   "MTd", //  link with LIBCMTD.LIB debug lib
+  "std", //  specify C++ language standard
   nullptr
 };