Merge pull request #4645 from hannes-steffenhagen-diffblue/feature-symtab_linking

Add symtab2gb to enable linking of .json_symtab files

Author: tautschnig

CMakeLists.txt

@@ -141,6 +141,7 @@ set_target_properties(
     linking
     pointer-analysis
     solvers
+    symtab2gb
     testing-utils
     unit
     util

regression/CMakeLists.txt

@@ -52,3 +52,4 @@ add_subdirectory(contracts)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
+add_subdirectory(symtab2gb)

regression/Makefile

@@ -27,6 +27,7 @@ DIRS = cbmc \
        contracts \
        goto-cc-file-local \
        linking-goto-binaries \
+       symtab2gb \
        # Empty last line
 
 # Run all test directories in sequence

regression/symtab2gb/CMakeLists.txt

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

regression/symtab2gb/Makefile

@@ -0,0 +1,27 @@
+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'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/symtab2gb/chain.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+symtab2gb_exe=$1
+cbmc_exe=$2
+
+$symtab2gb_exe "${@:3}"
+$cbmc_exe a.out

regression/symtab2gb/multiple_symtabs/README.md

@@ -0,0 +1,19 @@
+The `*.json_symtab` in this directory was created from the Ada source
+files `*.adb` using the
+[gnat2goto](https://github.com/diffblue/gnat2goto) compiler.
+
+```
+gnat2goto user.adb # produces user.json_symtab
+
+# produces library.json_symtab
+# and user.json_symtab
+# the --no-cprover-start option is to prevent
+# emitting a __CPROVER_start function for these modules,
+# as there can only be one of those in a program
+
+gnat2goto --no-cprover-start library.adb
+gnat2goto --no-cprover-start user.adb
+```
+
+Note that as of now, this requires the patch found in
+[this PR](https://github.com/diffblue/gnat2goto/pull/212)

regression/symtab2gb/multiple_symtabs/entry_point.adb

@@ -0,0 +1,7 @@
+with User;
+with Library;
+procedure Entry_Point is
+begin
+  User;
+  Library (-5);
+end Entry_Point;