Merge pull request #5935 from tautschnig/cpp-regression-test

Enable cpp-from-CVS regression tests

Author: tautschnig

regression/cpp-from-CVS/Address_of_Method1/main.cpp renamed to regression/cbmc-cpp/Address_of_Method1/main.cpp

@@ -1,3 +1,4 @@
+#include <cassert>
 struct x
 {
   void f();
@@ -11,7 +12,7 @@ void x::f()
 
 int main()
 {
-  assert(&x::f!=0);
+  assert(&x::f != 0);
 
-  assert(&x::i!=0);
+  assert(&x::i != 0);
 }

regression/cbmc-cpp/Address_of_Method1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG winbug macos-assert-broken
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-cpp/Anonymous_members1/main.cpp

@@ -0,0 +1,29 @@
+#include <cassert>
+typedef unsigned DWORD;
+typedef signed LONG;
+typedef long long LONGLONG;
+
+typedef union _LARGE_INTEGER {
+  struct
+  {
+    DWORD LowPart;
+    LONG HighPart;
+  };
+  struct
+  {
+    DWORD LowPart;
+    LONG HighPart;
+  } u;
+
+  LONGLONG QuadPart;
+} LARGE_INTEGER;
+
+int main()
+{
+  LARGE_INTEGER l;
+
+  l.QuadPart = 1;
+  l.LowPart = 2;
+  l.u.LowPart = 3;
+  assert(l.LowPart == 3);
+}

regression/cbmc-cpp/Anonymous_members1/test.desc

@@ -0,0 +1,8 @@
+CORE winbug macos-assert-broken
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-cpp/Array1/main.cpp

@@ -0,0 +1,10 @@
+int y[5][4][3][2];
+
+int main()
+{
+  for(int i = 0; i < 5; i++)
+    for(int j = 0; j < 4; j++)
+      for(int k = 0; k < 3; k++)
+        for(int l = 0; l < 2; l++)
+          y[i][j][k][l] = 2;
+}

regression/cpp-from-CVS/Array1/test.desc renamed to regression/cbmc-cpp/Array1/test.desc

@@ -0,0 +1,10 @@
+int y[2][3][4][5];
+
+int main()
+{
+  for(int i = 0; i < 5; i++)
+    for(int j = 0; j < 4; j++)
+      for(int k = 0; k < 3; k++)
+        for(int l = 0; l < 2; l++)
+          y[i][j][k][l] = 2; // out-of-bounds
+}

regression/cbmc-cpp/Array2/main.cpp

@@ -0,0 +1,11 @@
+struct C
+{
+  static const char *array[1];
+};
+
+const char *C::array[1] = {"HELLO"};
+
+int main(int argc, const char *argv[])
+{
+  assert(*C::array[0] == 'H');
+}