Restores corrupted regression tests from cbmc-cpp

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/cbmc-cpp/Lvalue1/main.cpp

@@ -0,0 +1,33 @@
+struct A
+{
+  int i;
+  A() : i(0)
+  {
+  }
+  int get_i()
+  {
+    return i;
+  }
+};
+
+A factory()
+{
+  return A();
+}
+
+int main()
+{
+  // Altough the returned value of `factory' is an
+  // rvalue, gcc accepts to bind it to the `this'
+  // parameter of the method `get_i'. Note that when used,
+  // a returned value is stored in a temporary
+  // (see goto_convertt::remove_function_call). Thus,
+  // the value returned by a function call can be treated
+  // as an lvalue.
+  //
+  // It's not clear what the best is. Should this code be rejected?
+  // Is the compatibility with gcc more important?
+
+  assert(factory().get_i() == 0);
+}
+

regression/cbmc-cpp/lvalue1/test.desc

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

regression/cbmc-cpp/typedef1/main.cpp

@@ -0,0 +1,23 @@
+#include <cassert>
+struct A
+{
+  int i;
+  A(int i) : i(i)
+  {
+  }
+};
+
+class B : public A
+{
+public:
+  typedef A _A;
+  B() : _A(0)
+  {
+  }
+};
+
+int main()
+{
+  B b;
+  assert(b.i == 0);
+}

regression/cbmc-cpp/typedef1/test.desc

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