Add tests of error handling on reading invalid goto binaries

Author: thomasspriggs

regression/CMakeLists.txt

@@ -56,6 +56,7 @@ add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
 add_subdirectory(goto-bmc/goto-bmc-symex-ready-goto)
 add_subdirectory(goto-bmc/goto-bmc-non-symex-ready-goto)
+add_subdirectory(goto-bmc)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 else()

regression/goto-bmc/CMakeLists.txt

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

regression/goto-bmc/invalid-files/not-goto-no-header.desc

@@ -0,0 +1,12 @@
+CORE
+not-goto-no-header.goto
+
+^EXIT=6$
+^SIGNAL=0$
+Please give exactly one binary file
+--
+not a goto binary
+Unable to read goto-binary from file not-goto-no-header\.goto
+--
+This test confirms that an appropriate error message is displayed in the case
+where a single input file is specified which does not pass the header check.

regression/goto-bmc/invalid-files/not-goto-no-header.goto

@@ -0,0 +1,2 @@
+This is not a goto binary. A header would be required to pass the
+`is_goto_binary` check.

regression/goto-bmc/invalid-files/not-goto-with-header.desc

@@ -0,0 +1,16 @@
+CORE
+not-goto-with-header.goto
+
+^EXIT=2$
+^SIGNAL=0$
+Unable to read goto-binary from file not-goto-with-header\.goto
+--
+Please give exactly one binary file
+not a goto binary
+--
+This test confirms that an appropriate error message is displayed in the case
+where an input file is specified which passed the header check used to
+determine if the file is a goto binary or not, but which is not followed by
+data of a valid goto binary file. Note that the `is_goto_binary` check works
+based on checking if the first four bytes of the file are the byte 7F followed
+by the characters "GBF".

regression/goto-bmc/invalid-files/not-goto-with-header.goto

@@ -0,0 +1,3 @@
+GBF
+This is not a valid goto binary. It does have a header which should pass the
+`is_goto_binary` check though.