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: peterschrammel

lib/cbmc

@@ -1,5 +1,6 @@
 DIRS = symex \
        symex-infeasibility \
+       goto-cc-symex \
        # Empty last line
 
 # Check for the existence of $dir. Tests under goto-gcc cannot be run on

regression/Makefile

@@ -0,0 +1,32 @@
+
+default: tests.log
+
+test:
+	@if ! ../../lib/cbmc/regression/test.pl -c ../chain.sh ; then \
+		../../lib/cbmc/regression/failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../../lib/cbmc/regression/test.pl -c ../chain.sh ; then \
+		../../lib/cbmc/regression/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/Makefile

@@ -0,0 +1,10 @@
+#!/bin/bash
+
+gc=../../../lib/cbmc/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/chain.sh

@@ -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/main.c

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

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

@@ -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/main.c

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

regression/symex/regenerate-entry-function/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

regression/symex/show-trace1/test.desc

@@ -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.cpp

@@ -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 \