Consolidate symtab2gb regression tests

Use an approach similar to contracts regression tests to extract
parameters for multiple tools from a single line in the .desc file. This
avoids overly fragmenting regression tests.

Author: tautschnig

regression/CMakeLists.txt

@@ -80,7 +80,6 @@ add_subdirectory(goto-cc-multi-file)
 add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
-add_subdirectory(symtab2gb-cbmc)
 add_subdirectory(solver-hardness)
 if(NOT WIN32)
   add_subdirectory(goto-ld)

regression/Makefile

@@ -53,7 +53,6 @@ DIRS = cbmc-shadow-memory \
        goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \
-       symtab2gb-cbmc \
        solver-hardness \
        goto-ld \
        validate-trace-xml-schema \

regression/symtab2gb-cbmc/CMakeLists.txt

@@ -1,4 +1,5 @@
 This directory contains tests based on converting json symtab files to goto
 binaries using the symtab2gb binary and then passing the generated goto binary
-to cbmc. Additional arguments specified in the `.desc` file will be passed to
-the symtab2gb binary.
+to cbmc. Additional arguments specified in the `.desc` file up until a possible
+`_` will be passed to the symtab2gb binary, any arguments specified after an `_`
+are passed to cbmc.

regression/symtab2gb-cbmc/Makefile

@@ -4,6 +4,22 @@ set -e
 
 symtab2gb_exe=$1
 cbmc_exe=$2
+source="${@: -1}"
+goto_binary="$source.gb"
 
-$symtab2gb_exe "${@:3}"
-$cbmc_exe a.out
+args=${*:3:$#-3}
+if [[ "$args" == *" _ "* ]]
+then
+  args_symtab="${args%%" _ "*}"
+  args_cbmc="${args#*" _ "}"
+elif [[ "$args" == "_ "* ]]
+then
+  args_symtab=""
+  args_cbmc="${args#"_ "}"
+else
+  args_symtab=$args
+  args_cbmc=""
+fi
+
+$symtab2gb_exe "$source" ${args_symtab} --out "$goto_binary"
+$cbmc_exe ${args_cbmc} "$goto_binary"

regression/symtab2gb-cbmc/README.md

@@ -1,6 +1,6 @@
 CORE
 rust.json
---json-ui --show-symbol-table
+ _ --json-ui --show-symbol-table
 "symbolTable":
 "mode": "rust",
 ^EXIT=0$

regression/symtab2gb-cbmc/chain.sh

@@ -1,6 +1,6 @@
 CORE
 rust.json
---show-symbol-table
+ _ --show-symbol-table
 Symbols:
 Mode\.+: rust
 ^EXIT=0$