Skip to content

Commit be17ef4

Browse files
martin-csmartin-cs
authored
Merge pull request #6293 from jezhiggins/vsd-max-array-length
VSD - max array length
2 parents 0bbbe19 + 63203b1 commit be17ef4

40 files changed

+732
-354
lines changed

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main(void)
2+
{
3+
int arr[] = {1, 2, 3, 4, 5};
4+
arr[2] = 99;
5+
int arr_0_after_write = arr[0];
6+
int arr_1_after_write = arr[1];
7+
int arr_2_after_write = arr[2];
8+
int arr_3_after_write = arr[3];
9+
int arr_4_after_write = arr[4];
10+
return 0;
11+
}

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> 1
7+
main::1::arr_1_after_write \(\) -> 2
8+
main::1::arr_2_after_write \(\) -> 99
9+
main::1::arr_3_after_write \(\) -> 4
10+
main::1::arr_4_after_write \(\) -> 5

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> TOP
7+
main::1::arr_1_after_write \(\) -> TOP
8+
main::1::arr_2_after_write \(\) -> TOP
9+
main::1::arr_3_after_write \(\) -> TOP
10+
main::1::arr_4_after_write \(\) -> TOP

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> 1
7+
main::1::arr_1_after_write \(\) -> 2
8+
main::1::arr_2_after_write \(\) -> TOP
9+
main::1::arr_3_after_write \(\) -> TOP
10+
main::1::arr_4_after_write \(\) -> TOP

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> \[1, 1\]
7+
main::1::arr_1_after_write \(\) -> \[2, 2\]
8+
main::1::arr_2_after_write \(\) -> \[63, 63\]
9+
main::1::arr_3_after_write \(\) -> \[4, 4\]
10+
main::1::arr_4_after_write \(\) -> \[5, 5\]

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> \[1, 63\]
7+
main::1::arr_1_after_write \(\) -> \[1, 63\]
8+
main::1::arr_2_after_write \(\) -> \[1, 63\]
9+
main::1::arr_3_after_write \(\) -> \[1, 63\]
10+
main::1::arr_4_after_write \(\) -> \[1, 63\]

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> \[1, 1\]
7+
main::1::arr_1_after_write \(\) -> \[2, 2\]
8+
main::1::arr_2_after_write \(\) -> \[3, 63\]
9+
main::1::arr_3_after_write \(\) -> \[3, 63\]
10+
main::1::arr_4_after_write \(\) -> \[3, 63\]

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
7+
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
8+
main::1::arr_2_after_write \(\) -> value-set-begin: 99 :value-set-end
9+
main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
10+
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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
7+
main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
8+
main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
9+
main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
10+
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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
7+
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
8+
main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
9+
main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
10+
main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end

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

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc

Lines changed: 0 additions & 7 deletions
This file was deleted.

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

Lines changed: 0 additions & 33 deletions
This file was deleted.

‎regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c renamed to ‎regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
int main(void)
22
{
3-
int arr[] = {1, 2, 3};
3+
int arr[] = {1, 2, 3, 4, 5};
44
int ix;
55
if(ix)
66
{
@@ -10,24 +10,25 @@ int main(void)
1010
{
1111
ix = 2;
1212
}
13+
1314
// ix is between 0 and 2
1415
// so this is between 1 and 3
1516
int arr_at_ix = arr[ix];
17+
1618
int write_ix;
1719
if(write_ix)
1820
{
1921
write_ix = 0;
2022
}
2123
else
2224
{
23-
write_ix = 1;
25+
write_ix = 4;
2426
}
25-
arr[write_ix] = 4;
27+
arr[write_ix] = 99;
2628
int arr_0_after_write = arr[0];
2729
int arr_1_after_write = arr[1];
28-
// We can't write to arr[2]
29-
// because write_ix is between 0 and 1
30-
// so this should be unchanged
3130
int arr_2_after_write = arr[2];
31+
int arr_3_after_write = arr[3];
32+
int arr_4_after_write = arr[4];
3233
return 0;
3334
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> TOP @ \[9\]
7+
main::1::arr_0_after_write \(\) -> TOP @ \[18\]
8+
main::1::arr_1_after_write \(\) -> TOP @ \[20\]
9+
main::1::arr_2_after_write \(\) -> TOP @ \[22\]
10+
main::1::arr_3_after_write \(\) -> TOP @ \[24\]
11+
main::1::arr_4_after_write \(\) -> TOP @ \[26\]

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> TOP @ \[9\]
7+
main::1::arr_0_after_write \(\) -> TOP
8+
main::1::arr_1_after_write \(\) -> TOP
9+
main::1::arr_2_after_write \(\) -> TOP
10+
main::1::arr_3_after_write \(\) -> TOP
11+
main::1::arr_4_after_write \(\) -> TOP

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> TOP @ \[9\]
7+
main::1::arr_0_after_write \(\) -> TOP
8+
main::1::arr_1_after_write \(\) -> TOP
9+
main::1::arr_2_after_write \(\) -> TOP
10+
main::1::arr_3_after_write \(\) -> TOP
11+
main::1::arr_4_after_write \(\) -> TOP

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\]
7+
main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\]
8+
main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\]
9+
main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\]
10+
main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\]
11+
main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\]

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
7+
main::1::arr_0_after_write \(\) -> \[1, 63\]
8+
main::1::arr_1_after_write \(\) -> \[1, 63\]
9+
main::1::arr_2_after_write \(\) -> \[1, 63\]
10+
main::1::arr_3_after_write \(\) -> \[1, 63\]
11+
main::1::arr_4_after_write \(\) -> \[1, 63\]

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
7+
main::1::arr_0_after_write \(\) -> \[1, 63\]
8+
main::1::arr_1_after_write \(\) -> \[2, 63\]
9+
main::1::arr_2_after_write \(\) -> \[3, 63\]
10+
main::1::arr_3_after_write \(\) -> \[3, 63\]
11+
main::1::arr_4_after_write \(\) -> \[3, 63\]

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> value-set-begin: 1, 3 :value-set-end
7+
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
8+
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
9+
main::1::arr_2_after_write \(\) -> value-set-begin: 3 :value-set-end
10+
main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
11+
main::1::arr_4_after_write \(\) -> value-set-begin: 5, 99 :value-set-end

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3, 4, 5 :value-set-end
7+
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
8+
main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
9+
main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
10+
main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
11+
main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::arr_at_ix \(\) -> value-set-begin: 1, 3, 4, 5 :value-set-end
7+
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
8+
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
9+
main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
10+
main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
11+
main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end

‎regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -339,10 +339,9 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
339339
type, top, bttm, e, environment, ns);
340340
}
341341

342-
abstract_object_pointert abstract_environmentt::add_object_context(
343-
const abstract_object_pointert &abstract_object) const
342+
const vsd_configt &abstract_environmentt::configuration() const
344343
{
345-
return object_factory->wrap_with_context(abstract_object);
344+
return object_factory->config();
346345
}
347346

348347
bool abstract_environmentt::merge(

‎src/analyses/variable-sensitivity/abstract_environment.h

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,8 @@ enum class widen_modet
3535
could_widen
3636
};
3737

38+
struct vsd_configt;
39+
3840
class abstract_environmentt
3941
{
4042
public:
@@ -174,18 +176,8 @@ class abstract_environmentt
174176
const exprt &e,
175177
const namespacet &ns) const;
176178

177-
/// Wraps an existing object in any configured context object
178-
///
179-
/// \param abstract_object: The object to be wrapped
180-
///
181-
/// \return The wrapped abstract object
182-
///
183-
/// Look at the configuration context dependency, and constructs
184-
/// the appropriate wrapper object around the supplied object
185-
/// If no such configuration is enabled, the supplied object will be
186-
/// returned unchanged
187-
virtual abstract_object_pointert
188-
add_object_context(const abstract_object_pointert &abstract_object) const;
179+
/// Exposes the environment configuration
180+
const vsd_configt &configuration() const;
189181

190182
/// Computes the join between "this" and "b"
191183
///

0 commit comments

Comments
 (0)