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

Author: Enrico Steffinlongo

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

@@ -0,0 +1,11 @@
+CORE gcc_only
+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 gcc_only is that it fails on certain windows system probably due to
+different interpretation of "".

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;
+}