Merge pull request #6293 from jezhiggins/vsd-max-array-length

VSD - max array length

Author: martin-cs

regression/goto-analyzer/variable-sensitivity-array-access/main.c

@@ -0,0 +1,11 @@
+int main(void)
+{
+  int arr[] = {1, 2, 3, 4, 5};
+  arr[2] = 99;
+  int arr_0_after_write = arr[0];
+  int arr_1_after_write = arr[1];
+  int arr_2_after_write = arr[2];
+  int arr_3_after_write = arr[3];
+  int arr_4_after_write = arr[4];
+  return 0;
+}

regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> 1
+main::1::arr_1_after_write \(\) -> 2
+main::1::arr_2_after_write \(\) -> 99
+main::1::arr_3_after_write \(\) -> 4
+main::1::arr_4_after_write \(\) -> 5

regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> TOP
+main::1::arr_1_after_write \(\) -> TOP
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP

regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> 1
+main::1::arr_1_after_write \(\) -> 2
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP

regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 1\]
+main::1::arr_1_after_write \(\) -> \[2, 2\]
+main::1::arr_2_after_write \(\) -> \[63, 63\]
+main::1::arr_3_after_write \(\) -> \[4, 4\]
+main::1::arr_4_after_write \(\) -> \[5, 5\]

regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 63\]
+main::1::arr_1_after_write \(\) -> \[1, 63\]
+main::1::arr_2_after_write \(\) -> \[1, 63\]
+main::1::arr_3_after_write \(\) -> \[1, 63\]
+main::1::arr_4_after_write \(\) -> \[1, 63\]

regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 1\]
+main::1::arr_1_after_write \(\) -> \[2, 2\]
+main::1::arr_2_after_write \(\) -> \[3, 63\]
+main::1::arr_3_after_write \(\) -> \[3, 63\]
+main::1::arr_4_after_write \(\) -> \[3, 63\]

regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 5 :value-set-end

regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end

regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end