Add regression tests for --export-symex-ready-goto

Author: Enrico Steffinlongo

regression/cbmc/CMakeLists.txt

@@ -1,26 +1,30 @@
 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   set(gcc_only -X gcc-only)
   set(gcc_only_string "-X;gcc-only;")
+  set(exclude_win_broken_tests -X winbug)
+  set(exclude_win_broken_tests_string "-X;winbug;")
 else()
   set(gcc_only "")
   set(gcc_only_string "")
+  set(exclude_win_broken_tests "")
+  set(exclude_win_broken_tests_string "")
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "cbmc-paths-lifo"
     "$<TARGET_FILE:cbmc> --paths lifo"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
 

regression/cbmc/export-symex-ready-goto/test-bad-usage.desc

@@ -0,0 +1,15 @@
+CORE winbug
+test.c
+--export-symex-ready-goto ""
+^ERROR: Please provide a filename to write the goto-binary to.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Ensure that --export-symex-ready-goto exported.symex-ready.goto terminates
+with error when incorrectly used.
+
+The reason why we use `winbug` is that it fails on certain windows system
+probably due to different interpretation of "". Not a bug, but we're using
+that label to remain consistent with other parts of the codebase, and not
+to unnecessarily introduce new ones for simple use cases.

regression/cbmc/export-symex-ready-goto/test-correct.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--export-symex-ready-goto exported.symex.ready.goto
+^Parsing test.c$
+^Converting$
+^Type-checking test$
+^Generating GOTO Program$
+^Removal of function pointers and virtual functions$
+^Generic Property Instrumentation$
+Exported goto-program in symex-ready-goto form at exported.symex.ready.goto
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that --export-symex-ready-goto exported.symex.ready.goto terminates successfully and logs this.

regression/cbmc/export-symex-ready-goto/test.c

@@ -0,0 +1,6 @@
+int main(int argc, char **argv)
+{
+  int arr[] = {0, 1, 2, 3, 4};
+  __CPROVER_assert(arr[0] == 1, "expected failure: 0 != 1");
+  return 0;
+}