Merge pull request #4014 from NlightNFotis/new_chain_sh

Add function harness generator and generator factory

Author: NlightNFotis

.gitignore

@@ -102,6 +102,8 @@ src/goto-cc/goto-cc
 src/goto-cc/goto-gcc
 src/goto-cc/goto-cc.exe
 src/goto-cc/goto-cl.exe
+src/goto-harness/goto-harness
+src/goto-harness/goto-harness.exe
 src/goto-instrument/goto-instrument
 src/goto-instrument/goto-instrument.exe
 src/solvers/smt2_solver

regression/goto-harness/CMakeLists.txt

@@ -1,2 +1,12 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
 add_test_pl_tests(
-  "$<TARGET_FILE:goto-harness>")
+  "../chain.sh \
+   $<TARGET_FILE:goto-cc> \
+   $<TARGET_FILE:goto-harness> \
+   $<TARGET_FILE:cbmc> \
+   ${is_windows}")

regression/goto-harness/Makefile

@@ -1,12 +1,24 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
 GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
+CBMC_EXE=../../../src/cbmc/cbmc
+
+ifeq ($(BUILD_ENV_),MSVC)
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
 
 test:
-	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 tests.log: ../test.pl
-	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 show:
 	@for dir in *; do \

regression/goto-harness/chain.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_harness=$2
+cbmc=$3
+is_windows=$4
+entry_point='generated_entry_function'
+
+name=${*:$#}
+name=${name%.c}
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+if [ -e "${name}-mod.gb" ] ; then
+  rm -f "${name}-mod.gb"
+fi
+
+$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
+$cbmc --function $entry_point "${name}-mod.gb"

regression/goto-harness/goto-harness-can-generate-trivial-harness/main.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int function_to_test(int some_argument)
+{
+  assert(some_argument == 0);
+  return some_argument;
+}

regression/goto-harness/goto-harness-can-generate-trivial-harness/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function function_to_test
+^\[function_to_test.assertion.1\] line \d+ assertion some_argument == 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/goto-harness/goto-harness-exists/test.desc

@@ -49,7 +49,7 @@ languages: util.dir langapi.dir \
 
 solvers.dir: util.dir
 
-goto-harness.dir: util.dir
+goto-harness.dir: util.dir goto-programs.dir
 
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir

src/Makefile

@@ -3,5 +3,6 @@ add_executable(goto-harness ${sources})
 generic_includes(goto-harness)
 
 target_link_libraries(goto-harness
-    util
+  util
+  goto-programs
 )

src/goto-harness/CMakeLists.txt

@@ -1,10 +1,17 @@
 SRC = \
+  function_call_harness_generator.cpp \
+  goto_harness_generator.cpp \
+  goto_harness_generator_factory.cpp \
   goto_harness_main.cpp \
   goto_harness_parse_options.cpp \
   # Empty last line
 
 OBJ += \
   ../util/util$(LIBEXT) \
+  ../goto-programs/goto-programs$(LIBEXT) \
+  ../big-int/big-int$(LIBEXT) \
+  ../langapi/langapi$(LIBEXT) \
+  ../linking/linking$(LIBEXT) \
   # Empty last line
 
 INCLUDES= -I ..