Cause a regeneration of the _start method if a --function is provided

appveyor.yml

@@ -74,6 +74,21 @@ test_script:
     sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
     cat goto-instrument-typedef/chain.sh || true
 
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
+    sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
+    sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
+    cat goto-cc-cbmc/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
+    cat goto-cc-goto-analyzer/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true
+    cat goto-cc-symex/chain.sh || true
+
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
     rmdir /s /q ansi-c\arch_flags_mcpu_good

regression/Makefile

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

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -4,9 +4,9 @@ main.c
 ^\*\* 7 of 7 covered \(100.0%\)$
 ^\*\* Used 4 iterations$
 ^Test suite:$
-^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
+^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
 --
 ^warning: ignoring

regression/cbmc/pointer-function-parameters/test.desc

@@ -4,8 +4,8 @@ main.c
 ^\*\* 5 of 5 covered \(100\.0%\)$
 ^\*\* Used 3 iterations$
 ^Test suite:$
-^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
-^a=&tmp\$1!0, tmp\$1=4$
-^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
+^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=4$
+^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
 --
 ^warning: ignoring

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/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,8 @@
+CORE
+main.c
+"--function fun --cover branch"
+^EXIT=0$
+^SIGNAL=0$
+^x=
+--
+^warning: ignoring

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

regression/symex/show-trace1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --trace
 ^EXIT=10$
@@ -9,3 +9,5 @@ main.c
 ^  k=6 .*$
 --
 ^warning: ignoring
+--
+diffblue/cbmc#1361