Merge pull request #5631 from jezhiggins/variable-sensitivity-option-passing

Variable sensitivity option passing

Author: martin-cs

regression/goto-analyzer/constant_propagation_08/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --simplify out.gb
+--variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$

regression/goto-analyzer/constant_propagation_09/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line \d+ a\[0\]==0: FAILURE \(if reachable\)$

regression/goto-analyzer/constant_propagation_10/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line 10 a\[0\]==2: FAILURE \(if reachable\)$

regression/goto-analyzer/constant_propagation_11/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --simplify out.gb
+--variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$

regression/goto-analyzer/constant_propagation_14/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] .* a\[0\]==1 || a\[0\]==2: SUCCESS$

regression/goto-analyzer/constant_propagation_15/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] .* a\[0\]==2: FAILURE \(if reachable\)$

regression/goto-analyzer/constant_propagation_18/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --verify --vsd-pointers
+--variable-sensitivity --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$

regression/goto-analyzer/constant_propagation_19/test-vsd.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --verify --vsd-pointers
+--variable-sensitivity --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$

regression/goto-analyzer/minimal-reproducer-for-struct-problem/test.desc

@@ -1,6 +1,6 @@
 CORE
 minimal_reproducer_for_struct_problem.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line 13 x.a==0: SUCCESS$

regression/goto-analyzer/sensitivity-function-call-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ assertion \*arr_y == 2: SUCCESS$

regression/goto-analyzer/sensitivity-function-call-opaque/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ assertion x == 3: SUCCESS$

regression/goto-analyzer/sensitivity-function-call-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ assertion y == 5: SUCCESS$

regression/goto-analyzer/sensitivity-function-call-primitive/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[bar\.assertion\.1\] line \d+ assertion other == 4: SUCCESS$

regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] .* assertion y==4: UNKNOWN$

regression/goto-analyzer/sensitivity-function-call-varargs/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ assertion y == 6: UNKNOWN$

regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_dependency_arrays.c
---variable-sensitivity  --vsd-arrays --vsd-pointers --vsd-structs --show
+--variable-sensitivity  --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show
 // Enable multi-line checking
 activate-multi-line-match
 ^EXIT=0$

regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_dependency_pointers.c
---variable-sensitivity  --vsd-arrays --vsd-pointers --vsd-structs --show
+--variable-sensitivity  --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show
 // Enable multi-line checking
 activate-multi-line-match
 ^EXIT=0$

regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_dependency_structs.c
---variable-sensitivity  --vsd-arrays --vsd-pointers --vsd-structs --show
+--variable-sensitivity  --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show
 // Enable multi-line checking
 activate-multi-line-match
 ^EXIT=0$

regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_dependency_variables.c
---variable-sensitivity  --vsd-arrays --vsd-pointers --vsd-structs --show
+--variable-sensitivity  --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]

regression/goto-analyzer/sensitivity-test-constants-array-loop/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line \d+ array\[0\] == 5: UNKNOWN$

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array_of_constants_array.c
---variable-sensitivity --vsd-arrays --verify --vsd-pointers
+--variable-sensitivity --vsd-arrays every-element --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]\[2\]==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array_of_constants_pointer.c
---variable-sensitivity --vsd-arrays --vsd-pointers --verify
+--variable-sensitivity --vsd-arrays every-element --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]==&a0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array_of_two_value_pointer.c
---variable-sensitivity --vsd-arrays --verify
+--variable-sensitivity --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]==&a0: UNKNOWN$

regression/goto-analyzer/sensitivity-test-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_array.c
---variable-sensitivity --vsd-arrays --verify --vsd-pointers
+--variable-sensitivity --vsd-arrays every-element --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* a\[1\]==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer_to_constants_array.c
---variable-sensitivity --vsd-pointers --vsd-arrays --verify
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* p==&a\[0\]: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer_to_constants_pointer.c
---variable-sensitivity --vsd-pointers --verify
+--variable-sensitivity --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* \*\*x==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer_to_constants_struct.c
---variable-sensitivity --vsd-pointers --vsd-structs --verify
+--variable-sensitivity --vsd-pointers constants --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] .* \(\*p\).a==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer_to_two_value_array.c
---variable-sensitivity --vsd-pointers --verify
+--variable-sensitivity --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* p==&a\[0\]: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer_to_two_value_struct.c
---variable-sensitivity --vsd-pointers --verify
+--variable-sensitivity --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* \(\*p\).a==0: UNKNOWN$

regression/goto-analyzer/sensitivity-test-constants-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_pointer.c
---variable-sensitivity --vsd-pointers --verify
+--variable-sensitivity --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x==&a: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct_of_constants_array.c
---variable-sensitivity --vsd-structs --vsd-arrays --verify
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.a\[0\]==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct_of_constants_pointer.c
---variable-sensitivity --vsd-structs --vsd-pointers --verify
+--variable-sensitivity --vsd-structs every-field --vsd-pointers constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.a==&a1: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct_of_constants_struct.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.s1.a==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct_of_two_value_array.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.a\[0\]==0: UNKNOWN$

regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct_of_two_value_pointer.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.a==&a1: UNKNOWN$

regression/goto-analyzer/sensitivity-test-constants-struct/test.desc

@@ -1,6 +1,6 @@
 CORE
 sensitivity_test_constants_struct.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] .* x.a==0: SUCCESS$

regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc

@@ -1,6 +1,6 @@
 CORE
 data-dependency-context.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-data-dependencies --show
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-data-dependencies --show
 // Enable multi-line checking
 activate-multi-line-match
 ^EXIT=0$

regression/goto-analyzer/sensitivity-test-struct-initialization/test.desc

@@ -1,6 +1,6 @@
 CORE
 struct-initialization.c
---variable-sensitivity --vsd-structs --verify
+--variable-sensitivity --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ los.a==0: SUCCESS$

regression/goto-analyzer/value-set-function-pointers-arrays/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check --three-way-merge
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge
 ^file main.c line 29 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 40 function main: replacing function pointer by 2 possible targets$
 ^main::1::fun1 \(\) -> value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$

regression/goto-analyzer/value-set-function-pointers-incremented/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check
 ^file main.c line 28 function main: replacing function pointer by 2 possible targets$
 ^main::1::fun_incremented_show \(\) -> TOP$
 ^EXIT=0$

regression/goto-analyzer/value-set-function-pointers-simple/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check --three-way-merge
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge
 ^file main.c line 25 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 28 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 33 function main: replacing function pointer by 2 possible targets$

regression/goto-analyzer/value-set-function-pointers-structs/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check
 ^file main.c line 38 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 46 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 54 function main: replacing function pointer by 2 possible targets$

regression/goto-analyzer/value-set-simple/test_show.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check
 ^global_int_show \(\) -> value-set-begin: [12], [12], :value-set-end$
 ^main::1::local_double_show \(\) -> value-set-begin: [12]\.0, [12]\.0, :value-set-end$
 ^main::1::local_double_ptr_show \(\) -> value-set-begin: ptr ->\(main::1::d[12]\), ptr ->\(main::1::d[12]\), :value-set-end$

regression/goto-analyzer/value-set-simple/test_verify.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --verify --pointer-check
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --verify --pointer-check
 ^\[main.assertion.1\] line 16 assertion global_int == 2: UNKNOWN$
 ^\[main.assertion.2\] line 17 assertion global_int == 1 \|\| global_int == 2: SUCCESS$
 ^\[main.assertion.3\] line 18 assertion global_int > 0: SUCCESS$

regression/goto-analyzer/value-set-structs/test_show.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --show --pointer-check
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check
 activate-multi-line-match
 main::1::s_show \(\) -> \{\.d=value-set-begin: [12]\.0, [12]\.0, :value-set-end, \.str=\{\[0\] = value-set-begin: '[xy]', '[xy]', :value-set-end\n\[1\] = value-set-begin: '\\n', :value-set-end
 main::1::u_show \(\) -> \{\.d=value-set-begin: [123]\.0, [123].0, [123]\.0, :value-set-end, \.str=\{\[0\] = value-set-begin: '[xyz]', '[xyz]', '[xyz]', :value-set-end\n\[1\] = value-set-begin: '\\n', :value-set-end

regression/goto-analyzer/value-set-structs/test_verify.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---variable-sensitivity --vsd-structs --vsd-arrays --vsd-pointers --vsd-value-sets --verify --pointer-check
+--variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --verify --pointer-check
 ^\[main\.assertion\.1\] line 33 assertion s\.i == 0: UNKNOWN$
 ^\[main\.assertion\.2\] line 35 assertion s\.d == 1.0: UNKNOWN$
 ^\[main\.assertion\.3\] line 36 assertion s\.d == 1.0 \|\| s.d == 2.0: SUCCESS$

regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity  --vsd-pointers --vsd-arrays --vsd-structs --unreachable-instructions
+--variable-sensitivity  --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --unreachable-instructions
 ^EXIT=0$
 ^SIGNAL=0$
 line 18 function func

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function pass_param --variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--function pass_param --variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 \[pass_param\.assertion\.1\] line 13 b\[0\]==0: SUCCESS

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-goto-after-function/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function test_param_function --variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--function test_param_function --variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 \[test_param_function.assertion\.1\] line \d+ a==5: SUCCESS

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-non-terminating-function/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function test_non_terminating --variable-sensitivity --vsd-pointers --vsd-arrays --vsd-structs --verify
+--function test_non_terminating --variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --vsd-structs every-field --verify
 ^EXIT=0$
 ^SIGNAL=0$
 \[test_non_terminating.assertion\.1\] line 23 one_val==5: SUCCESS