Merge pull request #5343 from NlightNFotis/feature/harness_dirty

Output C code from harness generation tool.

Author: NlightNFotis

regression/goto-harness/chain.sh

@@ -12,22 +12,28 @@ name=${*:$#}
 name=${name%.c}
 args=${*:5:$#-5}
 
+input_c_file="${name}.c"
+input_goto_binary="${name}.gb"
+harness_c_file="${name}-harness.c"
+
+
+
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+  $goto_cc "$input_c_file"
+  mv "${name}.exe" "$input_goto_binary"
 else
-  $goto_cc -o "${name}.gb" "${name}.c"
+  $goto_cc -o "$input_goto_binary" "$input_c_file"
 fi
 
-if [ -e "${name}-mod.gb" ] ; then
-  rm -f "${name}-mod.gb"
+if [ -e "$harness_c_file" ] ; then
+  rm -f "$harness_c_file"
 fi
 
 # `# some comment` is an inline comment - basically, cause bash to execute an empty command
-$cbmc --show-goto-functions "${name}.gb"
-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
-$cbmc --show-goto-functions "${name}-mod.gb"
-$cbmc --function $entry_point "${name}-mod.gb" \
+$cbmc --show-goto-functions "$input_goto_binary"
+$goto_harness "$input_goto_binary" "$harness_c_file" --harness-function-name $entry_point ${args}
+$cbmc --show-goto-functions "$harness_c_file"
+$cbmc --function $entry_point "$input_c_file" "$harness_c_file" \
   --pointer-check `# because we want to see out of bounds errors` \
   --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
   --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \

regression/goto-harness/constant-primitive/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void entry_point(const int x)
+{
+  // expected to succeed
+  assert(x - x == 0);
+
+  // expected to fail
+  assert(x != 13);
+}

regression/goto-harness/constant-primitive/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--function entry_point --harness-type call-function
+\[entry_point.assertion.1\] line \d+ assertion x - x == 0: SUCCESS
+\[entry_point.assertion.2\] line \d+ assertion x != 13: FAILURE
+^EXIT=10$
+^SIGNAL=0$

regression/goto-harness/constant-struct/test.c

@@ -0,0 +1,12 @@
+#include <stdlib.h>
+
+struct SomeStruct
+{
+  int x;
+};
+
+void entry_point(const struct SomeStruct value)
+{
+  assert(value.x - value.x == 0);
+  assert(value.x != 13);
+}

regression/goto-harness/constant-struct/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--function entry_point --harness-type call-function
+\[entry_point.assertion.1\] line \d+ assertion value.x - value.x == 0: SUCCESS
+\[entry_point.assertion.2\] line \d+ assertion value.x != 13: FAILURE
+^EXIT=10$
+^SIGNAL=0$

regression/goto-harness/havoc-global-int-02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
@@ -7,3 +7,5 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

regression/goto-harness/havoc-global-int-03/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
 ^EXIT=10$
@@ -8,3 +8,5 @@ main.c
 \[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

regression/goto-harness/havoc-global-struct/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
 ^EXIT=10$

regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$

regression/goto-harness/load-snapshot-static-global-array-01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$