Run cbmc c++ regression as part of default regression test

Set is_parameter for c++ function parameter symbol

Author: andreast271

regression/Makefile

@@ -1,6 +1,7 @@
 DIRS = ansi-c \
        cbmc \
        cbmc-cover \
+       cbmc-cpp \
        cbmc-java \
        cbmc-java-inheritance \
        cpp \

regression/cbmc-cpp/FunctionParam1/main.cpp

@@ -0,0 +1,12 @@
+#include <assert.h>
+int x;
+
+void g(int i){
+  x=i;
+}
+
+int main() {
+  g(3);
+  assert(x==3);
+}
+

regression/cbmc-cpp/FunctionParam1/test.desc

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

regression/cbmc-cpp/MethodParam1/main.cpp

@@ -0,0 +1,18 @@
+#include <assert.h>
+unsigned x;
+
+class ct {
+  void f(int i) {
+    x=x+i;
+  }
+};
+
+int main() {
+  unsigned r;
+  x=r%3;
+  ct c;
+  c.f(2);
+  assert(x<4);
+  assert(x<5);
+}
+

regression/cbmc-cpp/MethodParam1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.cpp
+
+instance is SATISFIABLE$
+instance is UNSATISFIABLE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-cpp/union2/main.cpp

@@ -1,3 +1,4 @@
+#include <assert.h>
 struct A
 {
   union

src/cpp/cpp_typecheck_function.cpp

@@ -44,8 +44,9 @@ void cpp_typecheckt::convert_parameter(
   symbol.type=parameter.type();
   symbol.is_state_var=true;
   symbol.is_lvalue=!is_reference(symbol.type);
+  symbol.is_parameter=true;
 
-  assert(!symbol.base_name.empty());
+  INVARIANT(!symbol.base_name.empty(), "parameter has base name");
 
   symbolt *new_symbol;