Added regression test for using --function on a GOTO program

Ensure that despite the prescence of a main method being compiled as the
entry point, we can still override it using --function in CBMC.

Author: thk123

regression/Makefile

@@ -5,6 +5,7 @@ DIRS = ansi-c \
        cbmc-java-inheritance \
        cpp \
        goto-analyzer \
+       goto-cc-cbmc \
        goto-diff \
        goto-gcc \
        goto-instrument \

regression/goto-cc-cbmc/Makefile

@@ -0,0 +1,30 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	@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) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/goto-cc-cbmc/chain.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+SRC=../../../src
+
+GC=$SRC/goto-cc/goto-cc
+CBMC=$SRC/cbmc/cbmc
+
+OPTS=$1
+NAME=${2%.c}
+
+$GC $NAME.c -o $NAME.gb
+$CBMC $NAME.gb $OPTS

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

@@ -0,0 +1,23 @@
+int fun(int x)
+{
+	if(x > 0)
+	{
+		return x * x;
+	}
+	else
+	{
+		return x;
+	}
+}
+
+int main(int argc, char** argv)
+{
+	if(argc>4)
+	{
+		return 0;
+	}
+	else
+	{
+		return 1;
+	}
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+"--function fun --cover branch"
+
+^EXIT=0$
+^SIGNAL=0$
+^x=
+--
+^warning: ignoring