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$

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

@@ -1,8 +1,10 @@
-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:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-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-1-snapshot.json --initial-goto-location main:0
 ^EXIT=10$
@@ -7,3 +7,5 @@ main.c
 \[main.assertion.2\] line [0-9]+ assertion y == 1: FAILURE
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

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

@@ -1,8 +1,10 @@
-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:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

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

@@ -1,8 +1,10 @@
-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$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-global-pointer-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$

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

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void entry_point(const int *x)
+{
+  if(x != NULL)
+  {
+    assert(*x - *x == 0);
+  }
+  // expected to fail because we should get non-null pointers
+  assert(x == NULL);
+}

regression/goto-harness/pointer-to-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 == .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$

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

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

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

@@ -0,0 +1,12 @@
+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$
+--
+--
+Note that the generated C code has a bug - the constant field actually isn't constant in CBMC.
+This is a bug that gets introduced somewhere in the C frontend, so we have no way of fixing this
+over here, but this test may have to be revisited once this has been resolved.

regression/snapshot-harness/arrays_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/arrays_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -9,3 +9,5 @@ p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/dynamic-array-int-ordering/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -14,3 +14,5 @@ a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type in
 VERIFICATION FAILED
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351

regression/snapshot-harness/dynamic-array-int/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -16,3 +16,4 @@ VERIFICATION FAILED
 unwinding assertion loop \d+: FAILURE
 --
 Broken by https://github.com/diffblue/cbmc/issues/4978
+For more information take a look at github#5351

regression/snapshot-harness/function_pointer_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -9,3 +9,5 @@ fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location m
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/function_pointer_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/function_pointer_03/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --ini
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/nondet_initialize_static_arrays/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer-to-array-char/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer-to-array-int/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -7,3 +7,5 @@ x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351

regression/snapshot-harness/pointer_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -10,3 +10,5 @@ x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-locatio
 \[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351