Merge pull request diffblue#1481 from andreast271/do-c++-regression

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

Author: tautschnig

appveyor.yml

@@ -83,6 +83,7 @@ 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

regression/CMakeLists.txt

@@ -25,10 +25,13 @@ endmacro(add_test_pl_tests)
 
 add_subdirectory(ansi-c)
 add_subdirectory(cbmc)
+add_subdirectory(cbmc-cover)
+add_subdirectory(cbmc-cpp)
 add_subdirectory(cbmc-java)
 add_subdirectory(cbmc-java-inheritance)
 add_subdirectory(cpp)
 add_subdirectory(goto-analyzer)
+add_subdirectory(goto-analyzer-taint)
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-diff)

regression/Makefile

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

regression/cbmc-cover/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-cpp/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

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

regression/goto-analyzer-taint/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:goto-analyzer>"
+)

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;