Fixed goto-instrument regressions

Author: esteffin

regression/goto-instrument/add-library1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---add-library --generate-function-body-options assert-false --generate-function-body '([^_]*)'
+--add-library --generate-function-body-options assert-false --generate-function-body '([^_]*)' _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

regression/goto-instrument/harness1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---model-argc-argv 3 --dump-c --harness
+--model-argc-argv 3 --dump-c --harness _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 Adding up to 3 command line arguments

regression/goto-instrument/insert-final-assert-false1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---insert-final-assert-false main
+--insert-final-assert-false main _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 insert-final-assert-false \(should fail\) : SUCCESS

regression/goto-instrument/labels1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--malloc-may-fail _ --no-standard-checks
 Labels: label_zero$
 Labels: label_one$
 Labels: label_two$

regression/goto-instrument/lexical-loops1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-lexical-loops
+--show-lexical-loops _ --no-standard-checks
 2 is head of \{ 2, 3, 4, 5 \(backedge\) \}
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-instrument/lexical-loops5/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-lexical-loops
+--show-lexical-loops _ --no-standard-checks
 2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 \(backedge\) \}
 5 is head of \{ 5, 6, 7, 8 \(backedge\) \}
 ^EXIT=0$

regression/goto-instrument/region-analysis-1/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-sese-regions
+--show-sese-regions _ --no-standard-checks
 ^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
 ^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$
 ^Function contains 2 single-entry, single-exit regions:$

regression/goto-instrument/region-analysis-2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-sese-regions
+--show-sese-regions _ --no-standard-checks
 ^Function contains 2 single-entry, single-exit regions:$
 ^Region starting at \(4, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$
 ^Region starting at \(0, [0-9]+\) IF .*7.* THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$

regression/goto-instrument/region-analysis-3/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-sese-regions
+--show-sese-regions _ --no-standard-checks
 ^Function contains 2 single-entry, single-exit regions:$
 ^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
 ^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$

regression/goto-instrument/region-analysis-9/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-sese-regions
+--show-sese-regions _ --no-standard-checks
 ^Function contains 2 single-entry, single-exit regions:$
 ^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(21, [0-9]+\) 6: ASSIGN main::argc := main::argc \+ 1$
 ^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 7 ends at \(24, [0-9]+\) 8: SKIP$

regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer-by-name fp/f,g
+--restrict-function-pointer-by-name fp/f,g _ --no-standard-checks
 \[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f, g)|(g, f)\]: SUCCESS
 \[main.assertion.1\] line \d+ assertion: FAILURE
 \[main.assertion.2\] line \d+ assertion: FAILURE

regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer-by-name main::1::fp/f
+--restrict-function-pointer-by-name main::1::fp/f _ --no-standard-checks
 \[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS
 \[main\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS
 f\(\)

regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer-by-name use_fp::fp/f
+--restrict-function-pointer-by-name use_fp::fp/f _ --no-standard-checks
 \[use_fp\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS
 \[use_fp\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS
 f\(\)

regression/goto-instrument/restrict-function-pointer-goto-target/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer main.function_pointer_call.1/f
+--restrict-function-pointer main.function_pointer_call.1/f _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.pointer_dereference.1\] line \d+ dereferenced function pointer must be f: SUCCESS

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer 'use_fg.function_pointer_call.1/f,g'
+--restrict-function-pointer 'use_fg.function_pointer_call.1/f,g' _ --no-standard-checks
 \[use_fg.assertion.1\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS
 \[use_fg.pointer_dereference.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: SUCCESS
 ^EXIT=0$

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer use_f.function_pointer_call.1/f,g
+--restrict-function-pointer use_f.function_pointer_call.1/f,g _ --no-standard-checks
 \[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g --restrict-function-pointer-by-name use_f::fptr/h
+--function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g --restrict-function-pointer-by-name use_f::fptr/h _ --no-standard-checks
 \[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function-pointer-restrictions-file restrictions.json
+--function-pointer-restrictions-file restrictions.json _ --no-standard-checks
 \[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---function-pointer-restrictions-file restrictions_1.json --function-pointer-restrictions-file restrictions_2.json
+--function-pointer-restrictions-file restrictions_1.json --function-pointer-restrictions-file restrictions_2.json _ --no-standard-checks
 \[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---restrict-function-pointer use_f.function_pointer_call.1/f
+--restrict-function-pointer use_f.function_pointer_call.1/f _ --no-standard-checks
 \[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-instrument/slice01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 2 --full-slice --add-library
+--no-malloc-may-fail --unwind 2 --full-slice --add-library _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice13/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice --add-library
+--full-slice --add-library _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice19/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice
+--full-slice _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice22/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice --add-library
+--no-malloc-may-fail --full-slice --add-library _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice23/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---full-slice --add-library
+--no-malloc-may-fail --full-slice --add-library _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice_general007/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---full-slice --add-library
+--full-slice --add-library --no-malloc-may-fail _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/goto-instrument/typedef4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---dump-c
+--dump-c _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-instrument/unwind-assert2/partial.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 9 --unwinding-assertions --partial-loops
+--unwind 9 --unwinding-assertions --partial-loops _ --no-standard-checks
 ^\[main.assertion.1\] line 6 fails when fully unwinding the loop: FAILURE$
 ^\*\* 2 of 2 failed
 ^EXIT=10$

regression/goto-instrument/unwind-assert2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 9 --unwinding-assertions
+--unwind 9 --unwinding-assertions _ --no-standard-checks
 ^\[main.assertion.1\] line 6 fails when fully unwinding the loop: SUCCESS$
 ^\*\* 1 of 2 failed
 ^EXIT=10$

regression/goto-instrument/value-set-fi-fp-removal4/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---value-set-fi-fp-removal
+--value-set-fi-fp-removal _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^file test.c line 20 function main: replacing function pointer by 2 possible targets$

regression/goto-instrument/value-set-fi-fp-removal5/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---value-set-fi-fp-removal
+--value-set-fi-fp-removal _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^file test.c line 19 function main: replacing function pointer by 0 possible targets$