Add --keep-implementations switch to goto-cc

The --keep-implementations switch takes a comma-separated list of
identifiers. When this switch is passed to goto-cc, the compiler will
not remove the symbols and definitions for the named functions, even
when they appear to be unused.

This patch is to support running CBMC on projects that define many of
their functions as static. Prior to this commit, users could not test
the correctness of functions marked as static because the function
definitions would not be exported by goto-cc.

Author: karkhaz

regression/CMakeLists.txt

@@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-cc-static)

regression/goto-cc-static/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-cc-static/chain.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+to_keep=""
+if [ $# -gt 3 ]; then
+  if [ $4!='' ]; then
+    to_keep="--keep-implementations $4"
+  fi
+fi
+
+cbmc_options=""
+if [ $# -gt 4 ]; then
+  cbmc_options=${*:5:$#-5}
+fi
+
+name=${*:$#}
+name=${name%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" ${to_keep} "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  "${goto_cc}" ${to_keep} "${name}.c" -o "${name}.gb"
+fi
+
+"${cbmc}" ${cbmc_options} "${name}.gb" ${cbmc_options}

regression/goto-cc-static/keep_static-1/main.c

@@ -0,0 +1,8 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+foo --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: foo$
+--
+^warning: ignoring

regression/goto-cc-static/keep_static-2/main.c

@@ -0,0 +1,8 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+main --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: main$
+--
+^Symbol......: foo$

regression/goto-cc-static/keep_static-3/main.c

@@ -0,0 +1,18 @@
+static int baz()
+{
+  return 3;
+}
+
+static int bar()
+{
+  return 3;
+}
+
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-3/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+foo,bar --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: foo$
+^Symbol......: bar$
+--
+^Symbol......: baz$

src/ansi-c/ansi_c_language.cpp

@@ -119,7 +119,7 @@ bool ansi_c_languaget::prv_typecheck(
     return true;
   }
 
-  if(remove_internal_symbols(new_symbol_table, *this))
+  if(remove_internal_symbols(new_symbol_table, symbols_to_keep, *this))
     return true;
 
   if(linking(symbol_table, new_symbol_table, get_message_handler()))