Merge pull request #6303 from thomasspriggs/tas/rust_mode

Enable usage of `--show-symbol-table` where the symbol table contains unrecognised modes.

Author: thomasspriggs

regression/CMakeLists.txt

@@ -67,6 +67,7 @@ add_subdirectory(goto-cc-file-local)
 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

@@ -42,6 +42,7 @@ DIRS = cbmc \
        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

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

regression/symtab2gb-cbmc/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc'
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/symtab2gb-cbmc/chain.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -e
+
+symtab2gb_exe=$1
+cbmc_exe=$2
+source="${@: -1}"
+goto_binary="$source.gb"
+cbmc_desc_arguments="${@:3:$#-3}"
+
+$symtab2gb_exe "$source" --out "$goto_binary"
+$cbmc_exe $cbmc_desc_arguments "$goto_binary"

regression/symtab2gb-cbmc/readme.md

@@ -0,0 +1,4 @@
+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 cbmc binary.

regression/symtab2gb-cbmc/show_foreign_symbol_table/json-ui.desc

@@ -0,0 +1,12 @@
+CORE
+rust.json
+--json-ui --show-symbol-table
+"symbolTable":
+"mode": "rust",
+^EXIT=0$
+^SIGNAL=0$
+--
+symbol \w+ has unknown mode
+--
+Test that --show-symbol-table with --json-ui correctly shows the source language
+mode of a symbol, even if that language mode is unsupported.

regression/symtab2gb-cbmc/show_foreign_symbol_table/plain_text.desc

@@ -0,0 +1,12 @@
+CORE
+rust.json
+--show-symbol-table
+Symbols:
+Mode\.+: rust
+^EXIT=0$
+^SIGNAL=0$
+--
+symbol \w+ has unknown mode
+--
+Test that --show-symbol-table correctly shows the source language mode of a
+symbol, even if that language mode is unsupported.