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