Fixed goto-harness regressions

Author: esteffin

Diff for: regression/goto-harness/array-types/test.desc

@@ -1,6 +1,6 @@
 CORE
 example.c
---harness-type call-function --function test --treat-pointer-as-array arr
+--harness-type call-function --function test --treat-pointer-as-array arr _ --no-standard-checks
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/goto-harness/associated-size-parameter/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type call-function --function test --associated-array-size array:size
+--harness-type call-function --function test --associated-array-size array:size _ --no-standard-checks
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/goto-harness/chain.sh

@@ -22,7 +22,14 @@ else
 fi
 
 args=${*:1:$#-1}
-
+if [[ "$args" != *" _ "* ]]
+then
+  args_harness=$args
+  args_cbmc=""
+else
+  args_harness="${args%%" _ "*}"
+  args_cbmc="${args#*" _ "}"
+fi
 
 cleanup()
 {
@@ -54,18 +61,20 @@ fi
 
 # `# some comment` is an inline comment - basically, cause bash to execute an empty command
 $cbmc --show-goto-functions "$input_goto_binary"
-$goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entry_point ${args}
+$goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entry_point ${args_harness}
 $cbmc --show-goto-functions "$harness_file"
 if [[ "${harness_file}" == "harness.gb" ]];then
   $cbmc --function $entry_point "$harness_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` \
+    ${args_cbmc} `# extra cbmc-related arguments` \
     # cbmc args end
 else
 $cbmc --function $entry_point "$input_c_file" "$harness_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` \
+  ${args_cbmc} `# extra cbmc-related arguments` \
   # cbmc args end
 fi

Diff for: regression/goto-harness/do-not-use-nondet-for-recursion/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function test --harness-type call-function
+--function test --harness-type call-function _ --no-standard-checks
 \[test.assertion.1\] line \d+ assertion list: SUCCESS
 \[test.assertion.2\] line \d+ assertion list->next: FAILURE
 \[test.assertion.3\] line \d+ assertion !\(list->next != \(\(struct linked_list \*\).*\)\): FAILURE

Diff for: regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function test --harness-type call-function --treat-pointers-equal x,y --treat-pointers-equal-maybe
+--function test --harness-type call-function --treat-pointers-equal x,y --treat-pointers-equal-maybe _ --no-standard-checks
 should_make_equal
 \[test.assertion.1\] line 3 assertion x: SUCCESS
 \[test.assertion.2\] line 4 assertion y: SUCCESS

Diff for: regression/goto-harness/mixed-constructors/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function entry_point --harness-type call-function --associated-array-size array_with_size:size
+--function entry_point --harness-type call-function --associated-array-size array_with_size:size _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 --

Diff for: regression/goto-harness/nondet_elements_longer_lists/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function
+--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function _ --no-standard-checks
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/goto-harness/nondet_elements_longer_lists_global/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals
+--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals _ --no-standard-checks
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/goto-harness/nondet_initialize_static_arrays/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 4 --harness-type call-function
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 4 --harness-type call-function _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/nondet_strings/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type call-function --function function --treat-pointer-as-cstring pointer --associated-array-size pointer:size
+--harness-type call-function --function function --treat-pointer-as-cstring pointer --associated-array-size pointer:size _ --no-standard-checks
 \[function.assertion.\d+\] line \d+ assertion pointer\[size - 1\] == \'\\0\': SUCCESS
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

Diff for: regression/goto-harness/nondet_strings_should_only_have_zero_at_end/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length
+--harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length _ --no-standard-checks
 \[calling_func.assertion.\d+\] line \d+ assertion stringlength\(s\) \+ 1 == length: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

Diff for: regression/goto-harness/pointer-function-parameters-equal-maybe/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' --treat-pointers-equal-maybe
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' --treat-pointers-equal-maybe _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[func.assertion.\d+\] line \d+ assertion p == q: FAILURE$

Diff for: regression/goto-harness/pointer-function-parameters-equal-simple/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t'
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t' _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --harness-type call-function
+--function func --min-null-tree-depth 10 --harness-type call-function _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 \[func.assertion.1\] line [0-9]+ assertion p != .*((NULL)|0).*: SUCCESS

Diff for: regression/goto-harness/pointer-function-parameters-struct-simple-recursion-2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 2  --harness-type call-function
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 2  --harness-type call-function _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/pointer-function-parameters-struct-simple-recursion/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz
+--harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz _ --no-standard-checks
 \[test.assertion.1\] line \d+ assertion sz < 10: FAILURE
 \[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS
 \[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS

Diff for: regression/goto-harness/pointer-to-array-function-parameters-min-size/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function min_array_size_test --max-array-size 3 --min-array-size 3 --associated-array-size arr:sz
+--harness-type call-function --function min_array_size_test --max-array-size 3 --min-array-size 3 --associated-array-size arr:sz _ --no-standard-checks
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/goto-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
+--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5 _ --no-standard-checks
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
+--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS

Diff for: regression/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function test --treat-pointer-as-array arr
+--harness-type call-function --function test --treat-pointer-as-array arr _ --no-standard-checks
 \[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?0\]: SUCCESS
 \[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?10\]: FAILURE
 ^EXIT=10$

Diff for: regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function func --min-null-tree-depth 10 --max-nondet-tree-depth 1  --harness-type call-function
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 1  --harness-type call-function _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL