Enable cpp-from-CVS regression tests

regression/cpp-from-CVS/Address_of_Method1/main.cpp → 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/cbmc-cpp/Array2/main.cpp

@@ -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/Array3/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');
+}

regression/cpp-from-CVS/Array4/elsewhere.cpp → regression/cbmc-cpp/Array4/elsewhere.cpp

@@ -4,5 +4,5 @@ void elsewhere()
 {
   char ch;
   // should fail, this is out of bounds
-  ch=my_string[10];
+  ch = my_string[10];
 }

regression/cpp-from-CVS/Array4/main.cpp → regression/cbmc-cpp/Array4/main.cpp

@@ -1,4 +1,4 @@
-char my_string[]="abc";
+char my_string[] = "abc";
 
 void elsewhere();
 

regression/cpp-from-CVS/Assignment1/main.cpp → regression/cbmc-cpp/Assignment1/main.cpp

@@ -1,9 +1,13 @@
-struct A { int i;};
+#include <cassert>
+struct A
+{
+  int i;
+};
 
 struct B
 {
   int i;
-  B& operator = (const B& b)
+  B &operator=(const B &b)
   {
     i = b.i;
     return *this;
@@ -17,7 +21,6 @@ A funcA()
   return a;
 }
 
-
 B funcB()
 {
   B b;
@@ -33,5 +36,5 @@ int main()
 
   B b;
   b.i = 20;
-  assert((funcB() = b).i == 20);  // legal
+  assert((funcB() = b).i == 20); // legal
 }

regression/cbmc-cpp/Assignment1/test.desc

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

regression/cpp-from-CVS/Class_Members1/main.cpp → regression/cbmc-cpp/Class_Members1/main.cpp

@@ -1,28 +1,29 @@
+#include <cassert>
 class t
 {
 public:
   int i;
   void f();
 
-  void g(double xxx=3.2);
+  void g(double xxx = 3.2);
 };
 
 void t::f()
 {
-  i=1;
+  i = 1;
 }
 
 void t::g(double d)
 {
-  i=(int)d;
+  i = (int)d;
 }
 
 int main()
 {
   t instance;
   instance.f();
-  assert(instance.i==1);
+  assert(instance.i == 1);
 
   instance.g(2.1);
-  assert(instance.i==2);
+  assert(instance.i == 2);
 }

regression/cbmc-cpp/Class_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/Comma_Operator1/main.cpp

@@ -0,0 +1,9 @@
+#include <cassert>
+int main()
+{
+  int s = 0;
+  int t = 0;
+  t = (s = 3, s + 2);
+  assert(s == 3);
+  assert(t == 5);
+}

regression/cbmc-cpp/Comma_Operator1/test.desc

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

regression/cbmc-cpp/ConditionalExpression1/main.cpp

@@ -0,0 +1,13 @@
+#include <cassert>
+int main()
+{
+  bool b;
+  int a = 0;
+  int c = 0;
+
+  b ? a += 1 : c += 1;
+
+  assert(a == 1 || a == 0);
+  assert(c == 1 || c == 0);
+  assert(a != c);
+}

regression/cbmc-cpp/ConditionalExpression1/test.desc

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

regression/cpp-from-CVS/ConditionalExpression2/main.cpp → regression/cbmc-cpp/ConditionalExpression2/main.cpp

@@ -1,9 +1,10 @@
+#include <cassert>
 char a[1];
 char b[2];
 
 int main()
 {
-  char* c = true ? a : b;
+  char *c = true ? a : b;
   assert(*c == a[0]);
   return 0;
 }

regression/cbmc-cpp/ConditionalExpression2/test.desc

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

regression/cpp-from-CVS/Constant5/main.cpp → regression/cbmc-cpp/Constant5/main.cpp

@@ -1,9 +1,9 @@
-const int ASD1=1;
+const int ASD1 = 1;
 
 int array[ASD1];
 
 int main()
 {
   // this sound fail!
-  (int &)ASD1=2;
+  (int &)ASD1 = 2;
 }

regression/cbmc-cpp/Constructor1/main.cpp

@@ -0,0 +1,49 @@
+#include <cassert>
+class t1
+{
+public:
+  int i;
+
+  t1()
+  {
+    i = 1;
+  }
+};
+
+class t2
+{
+public:
+  int i;
+
+  t2() : i(2)
+  {
+  }
+};
+
+class t3
+{
+public:
+  int i;
+
+  t3();
+};
+
+t3::t3() : i(3)
+{
+}
+
+int main()
+{
+  t1 instance1;
+  assert(instance1.i == 1);
+
+  t2 instance2;
+  assert(instance2.i == 2);
+
+  t2 *p = new t2;
+  assert(p->i == 2);
+  delete p;
+
+  t3 instance3;
+  assert(instance3.i == 3);
+}

regression/cbmc-cpp/Constructor1/test.desc

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

regression/cpp-from-CVS/Constructor10/main.cpp → regression/cbmc-cpp/Constructor10/main.cpp

@@ -1,14 +1,17 @@
 class A
 {
-  public:
+public:
   int a;
-  A(int a):a(a){}
+  A(int a) : a(a)
+  {
+  }
 };
 
-
 A f()
 {
   return A(0);
 }
 
-int main() {}
+int main()
+{
+}

regression/cbmc-cpp/Constructor12/main.cpp

@@ -0,0 +1,30 @@
+#include <cassert>
+struct A
+{
+  int i;
+  A() : i(10)
+  {
+  }
+
+private:
+  A(const A &a); // disabled
+};
+
+class B : A
+{
+public:
+  B(){};
+  int get_i()
+  {
+    return i;
+  }
+
+private:
+  B(B &b); // disabled
+};
+
+int main()
+{
+  B b;
+  assert(b.get_i() == 10);
+}

regression/cbmc-cpp/Constructor12/test.desc

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