Add regression tests for --extract-core-goto

Author: Enrico Steffinlongo

regression/cbmc/export-core-goto/test-bad-usage-2.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--export-core-goto ""
+^ERROR: Please provide a filename to write the goto-binary to.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Ensure that --export-core-goto exported.core.goto terminates with error when incorrectly used.

regression/cbmc/export-core-goto/test-correct.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--export-core-goto exported.core.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 core-goto form at exported.core.goto
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that --export-core-goto exported.core.goto terminates successfully and logs this.

regression/cbmc/export-core-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;
+}