Add support for using the --function flag to goto-analyze and symex

symex and goto-analyze (through the goto_modelt class) now support
setting the --function flag on precompiled .gb files.

Refactored out the function flag and its help function to
rebuild_goto_start_functions.

Used this extracted flag in goto-analyze, symex and CBMC.

Added tests that check both goto-analyze and symex when ran with the
--function flag actually generate the correct _start function. Also
added tests for when it isn't a precompiled binary. Added these new
folders to the overal test suite

Author: thk123

regression/Makefile

@@ -6,6 +6,8 @@ DIRS = ansi-c \
        cpp \
        goto-analyzer \
        goto-cc-cbmc \
+       goto-cc-goto-analyzer \
+       goto-cc-goto-symex \
        goto-diff \
        goto-gcc \
        goto-instrument \

regression/goto-analyzer/regenerate-entry-function/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}

regression/goto-analyzer/regenerate-entry-function/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function fun --show-goto-functions
+^\s*fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-cc-cbmc/regenerate-entry-function/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 "--function fun --cover branch"
-
 ^EXIT=0$
 ^SIGNAL=0$
 ^x=

regression/goto-cc-goto-analyzer/Makefile

@@ -0,0 +1,32 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-goto-analyzer/chain.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+src=../../../src
+
+gc=$src/goto-cc/goto-cc
+goto_analyzer=$src/goto-analyzer/goto-analyzer
+
+options=$1
+name=${2%.c}
+
+$gc $name.c -o $name.gb
+$goto_analyzer $name.gb $options

regression/goto-cc-goto-analyzer/regenerate-entry-function/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}

regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--function fun --show-goto-functions"
+^\s*fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-cc-symex/Makefile

@@ -0,0 +1,32 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-symex/chain.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+src=../../../src
+
+gc=$src/goto-cc/goto-cc
+symex=$src/symex/symex
+
+options=$1
+name=${2%.c}
+
+$gc $name.c -o $name.gb
+$symex $name.gb $options

regression/goto-cc-symex/regenerate-entry-function/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}

regression/goto-cc-symex/regenerate-entry-function/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--function fun --show-goto-functions"
+^\s*return.=fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/symex/regenerate-entry-function/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}

regression/symex/regenerate-entry-function/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function fun --show-goto-functions
+fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -1009,7 +1009,7 @@ void cbmc_parse_optionst::help()
     " --round-to-plus-inf          rounding towards plus infinity\n"
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --round-to-zero              rounding towards zero\n"
-    " --function name              set main function name\n"
+    HELP_FUNCTIONS
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"

src/cbmc/cbmc_parse_options.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -26,7 +27,8 @@ class goto_functionst;
 class optionst;
 
 #define CBMC_OPTIONS \
-  "(program-only)(function):(preprocess)(slice-by-trace):" \
+  "(program-only)(preprocess)(slice-by-trace):" \
+  OPT_FUNCTIONS \
   "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -494,6 +494,7 @@ void goto_analyzer_parse_optionst::help()
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
+    HELP_FUNCTIONS
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -27,7 +28,7 @@ class goto_functionst;
 class optionst;
 
 #define GOTO_ANALYSER_OPTIONS \
-  "(function):" \
+  OPT_FUNCTIONS \
   "D:I:(std89)(std99)(std11)" \
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \

src/goto-programs/rebuild_goto_start_function.cpp

@@ -69,7 +69,7 @@ bool rebuild_goto_start_functiont::operator()(
       symbol_table);
 
   // Remove the function from the goto_functions so it is copied back in
-  // from the symbol table
+  // from the symbol table during goto_convert
   if(!return_code)
   {
     const auto &start_function=

src/goto-programs/rebuild_goto_start_function.h

@@ -14,6 +14,12 @@
 class symbol_tablet;
 class goto_functionst;
 
+#define OPT_FUNCTIONS \
+  "(function):"
+
+#define HELP_FUNCTIONS \
+  " --function name              set main function name\n"
+
 class rebuild_goto_start_functiont: public messaget
 {
 public:

src/symex/symex_parse_options.cpp

@@ -587,7 +587,7 @@ void symex_parse_optionst::help()
     " --round-to-plus-inf          IEEE floating point rounding mode\n"
     " --round-to-minus-inf         IEEE floating point rounding mode\n"
     " --round-to-zero              IEEE floating point rounding mode\n"
-    " --function name              set main function name\n"
+    HELP_FUNCTIONS
     "\n"
     "Java Bytecode frontend options:\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP

src/symex/symex_parse_options.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -28,7 +29,7 @@ class goto_functionst;
 class optionst;
 
 #define SYMEX_OPTIONS \
-  "(function):" \
+  OPT_FUNCTIONS \
   "D:I:" \
   "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
   OPT_GOTO_CHECK \