Add regression tests for new goto-inspect binary

Author: NlightNFotis

regression/CMakeLists.txt

@@ -46,6 +46,7 @@ add_subdirectory(goto-instrument-chc)
 add_subdirectory(goto-instrument-json)
 add_subdirectory(goto-instrument-wmm-core)
 add_subdirectory(goto-instrument-typedef)
+add_subdirectory(goto-inspect)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)
 add_subdirectory(strings)

regression/goto-inspect/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect>"
+)

regression/goto-inspect/chain.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+# A test instruction passed to this `chain.sh` file looks like this:
+# 
+# build/bin/goto-cc build/bin/goto-inspect --show-goto-functions main.c
+#
+# This allows us to safely assume for now (as long as we're operating
+# goto-inspect with one binary and one inspection option, which seems
+# to be the case for now) that the option is going to be at $3.
+# If this is no longer the case in the future, this script will need
+# to be made significantly more sophisticated in terms of handling
+# a variable number of options for the goto-inspect binary.
+
+echo $@
+
+goto_cc_exe=$1
+goto_inspect_exe=$2
+
+name=${*:$#}
+name=${name%.c}
+
+$goto_cc_exe -o "${name}.gb" "${name}.c"
+$goto_inspect_exe $3 "${name}.gb" 

regression/goto-inspect/show-goto-functions/main.c

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

regression/goto-inspect/show-goto-functions/negative.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+" "
+^EXIT=6$
+^SIGNAL=0$
+--
+DECL main::1::arr : signedbv\[32\]\[5\]
+ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
+ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
+DEAD main::1::arr
+SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
+END_FUNCTION
+--
+This is testing the behaviour of the goto-inspect binary in case a binary
+is present, but no inspection option is present.

regression/goto-inspect/show-goto-functions/positive.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main
+DECL main::1::arr : signedbv\[32\]\[5\]
+ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
+ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
+DEAD main::1::arr
+SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
+END_FUNCTION
+--
+--

src/goto-inspect/goto_inspect_parse_options.cpp

@@ -62,13 +62,13 @@ int goto_inspect_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  // If an option + binary was provided, the program will have exited gracefully
-  // through a different branch. If we hit the code below, it means that something
-  // has gone wrong - it's also possible to fall through this case if no optional
-  // inspection flag is present in the argument vector. This will ensure that the
-  // return value in that case is semantically meaningful, and provide a return
-  // value that also satisfies the compiler's requirements based on the signature
-  // of `doit()`.
+  // If an option + binary was provided, the program will have exited
+  // gracefully through a different branch. If we hit the code below, it
+  // means that something has gone wrong - it's also possible to fall through
+  // this case if no optional inspection flag is present in the argument
+  // vector. This will ensure that the return value in that case is
+  // semantically meaningful, and provide a return value that also satisfies
+  // the compiler's requirements based on the signature of `doit()`.
   return CPROVER_EXIT_INCORRECT_TASK;
 }