Skip to content

Commit fd6cef4

Browse files
feliperodrifeliperodri
committed
Adds regression test to cover ranges support
Code contracts properly supports assigns clause with array ranges. So, we added regression tests to validate this capability. Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 31c40d8 commit fd6cef4

File tree

34 files changed

+377
-37
lines changed

34 files changed

+377
-37
lines changed

‎regression/contracts/assigns_enforce_arrays_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
void f1(int a[], int len) __CPROVER_assigns(a)
1+
/* clang-format off */
2+
void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
3+
/* clang-format on */
24
{
35
int b[10];
46
a = b;

‎regression/contracts/assigns_enforce_arrays_02/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,9 @@ int nextIdx() __CPROVER_assigns(idx)
88
return idx;
99
}
1010

11-
void f1(int a[], int len)
11+
/* clang-format off */
12+
void f1(int a[], int len) __CPROVER_assigns(idx, a[2 .. 5])
13+
/* clang-format on */
1214
{
1315
a[nextIdx()] = 5;
1416
}

‎regression/contracts/assigns_enforce_arrays_03/main.c

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,16 @@
1-
void assign_out_under(int a[], int len) __CPROVER_assigns(a)
1+
/* clang-format off */
2+
void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
3+
/* clang-format on */
24
{
3-
a[1] = 5;
5+
int *indr;
6+
indr = a + 3;
7+
*indr = 5;
48
}
59

610
int main()
711
{
812
int arr[10];
9-
assign_out_under(arr, 10);
13+
f1(arr, 10);
1014

1115
return 0;
1216
}

‎regression/contracts/assigns_enforce_arrays_03/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE
22
main.c
33
--enforce-all-contracts
4-
^EXIT=10$
4+
^EXIT=0$
55
^SIGNAL=0$
6-
^VERIFICATION FAILED$
6+
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
Checks whether verification fails when an array is assigned at an index
10-
below its lower bound.
9+
Checks whether verification succeeds when an array is assigned indirectly
10+
through a pointer.

‎regression/contracts/assigns_enforce_arrays_04/main.c

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,28 @@
1-
void assigns_single(int a[], int len) __CPROVER_assigns(a)
1+
void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
22
{
3+
a[8] = 20;
34
}
45

5-
void assigns_range(int a[], int len) __CPROVER_assigns(a)
6+
/* clang-format off */
7+
void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
8+
/* clang-format on */
69
{
10+
a[5] = 10;
711
}
812

9-
void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
13+
/* clang-format off */
14+
void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
15+
/* clang-format oon */
1016
{
11-
assigns_single(a, len);
12-
assigns_range(a, len);
17+
a[2] = 10;
1318
}
1419

1520
int main()
1621
{
1722
int arr[10];
18-
assigns_big_range(arr, 10);
23+
assigns_upper_bound(arr, 10);
24+
assigns_lower_bound(arr, 10);
25+
assigns_single(arr, 10);
1926

2027
return 0;
2128
}

‎regression/contracts/assigns_enforce_arrays_04/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
Checks whether verification succeeds when an array is assigned through
10-
calls to functions with array assigns clauses which are compatible with
11-
that of the caller.
9+
Checks whether verification succeeds when an array is assigned at both upper
10+
and lower bounds of its assignable array range. Single-value array range
11+
assignment is checked as well.

‎regression/contracts/assigns_enforce_arrays_05/main.c

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,14 @@
1-
void assigns_ptr(int *x) __CPROVER_assigns(*x)
1+
/* clang-format off */
2+
void assign_out_under(int a[], int len) __CPROVER_assigns(a[2 .. 5])
3+
/* clang-format on */
24
{
3-
*x = 200;
4-
}
5-
6-
void assigns_range(int a[], int len) __CPROVER_assigns(a)
7-
{
8-
int *ptr = &(a[7]);
9-
assigns_ptr(ptr);
5+
a[1] = 5;
106
}
117

128
int main()
139
{
1410
int arr[10];
15-
assigns_range(arr, 10);
11+
assign_out_under(arr, 10);
1612

1713
return 0;
1814
}

‎regression/contracts/assigns_enforce_arrays_05/test.desc

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,5 @@ main.c
66
^VERIFICATION FAILED$
77
--
88
--
9-
Checks whether verification fails when an array is assigned via a
10-
function call which assigns a pointer to an element out of the
11-
allowable range.
9+
Checks whether verification fails when an array is assigned at an index
10+
below its lower bound.

‎regression/contracts/assigns_enforce_arrays_06/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
2+
{
3+
a[7] = 5;
4+
}
5+
6+
int main()
7+
{
8+
int arr[10];
9+
assign_out_under(arr, 10);
10+
11+
return 0;
12+
}

‎regression/contracts/assigns_enforce_arrays_06/test.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+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when an array is assigned at an index below
10+
its allowed index and specification contains only a single cell
11+
instead of a range.

‎regression/contracts/assigns_enforce_arrays_07/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
/* clang-format off */
2+
void assign_out_over(int a[], int len) __CPROVER_assigns(a[2 .. 5])
3+
/* clang-format on */
4+
{
5+
a[6] = 5;
6+
}
7+
8+
int main()
9+
{
10+
int arr[10];
11+
assign_out_over(arr, 10);
12+
13+
return 0;
14+
}

‎regression/contracts/assigns_enforce_arrays_07/test.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+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when an array is assigned at an index
10+
above its upper bound.

‎regression/contracts/assigns_enforce_arrays_08/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
2+
{
3+
a[9] = 5;
4+
}
5+
6+
int main()
7+
{
8+
int arr[10];
9+
assign_out_under(arr, 10);
10+
11+
return 0;
12+
}

‎regression/contracts/assigns_enforce_arrays_08/test.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+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when an array is assigned at an index
10+
above its allowed index.

‎regression/contracts/assigns_enforce_arrays_09/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
/* clang-format off */
2+
void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
3+
/* clang-format on */
4+
{
5+
a[last_idx] = 6;
6+
}
7+
8+
int main()
9+
{
10+
int arr[10];
11+
assigns_in_range(arr, 9);
12+
13+
return 0;
14+
}

‎regression/contracts/assigns_enforce_arrays_09/test.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+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks whether verification succeeds when an array is assigned at the upper
10+
bounds of its assignable array range, when the range has a non-constant bound.

‎regression/contracts/assigns_enforce_arrays_10/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
/* clang-format off */
2+
void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
3+
/* clang-format on */
4+
{
5+
last_idx++;
6+
a[last_idx] = 6;
7+
}
8+
9+
int main()
10+
{
11+
int arr[10];
12+
assigns_in_range(arr, 9);
13+
14+
return 0;
15+
}

‎regression/contracts/assigns_enforce_arrays_10/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when an array is assigned past the upper
10+
bound of its assignable array range, using the symbol of the upper bound,
11+
after it has been incremented. This is intended to show that the bounds
12+
are determined at the time the function is called.

‎regression/contracts/assigns_enforce_arrays_11/main.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
void assigns_single(int a[], int len) __CPROVER_assigns(a[7])
2+
{
3+
}
4+
5+
/* clang-format off */
6+
void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
7+
/* clang-format on */
8+
{
9+
}
10+
11+
/* clang-format off */
12+
void assigns_big_range(int a[], int len) __CPROVER_assigns(a[2 .. 7])
13+
/* clang-format on */
14+
{
15+
assigns_single(a, len);
16+
assigns_range(a, len);
17+
}
18+
19+
int main()
20+
{
21+
int arr[10];
22+
assigns_big_range(arr, 10);
23+
24+
return 0;
25+
}

‎regression/contracts/assigns_enforce_arrays_11/test.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+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks whether verification succeeds when an array is assigned through
10+
calls to functions with array assigns clauses which are compatible with
11+
that of the caller.

‎regression/contracts/assigns_enforce_arrays_12/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
/* clang-format off */
2+
void assign_25(int a[], int len) __CPROVER_assigns(a[2 .. 5])
3+
/* clang-format on */
4+
{
5+
}
6+
7+
/* clang-format off */
8+
void assign_37(int a[], int len) __CPROVER_assigns(a[3 .. 7])
9+
/* clang-format on */
10+
{
11+
assign_25(a, len);
12+
}
13+
14+
int main()
15+
{
16+
int arr[10];
17+
assign_37(arr, 10);
18+
19+
return 0;
20+
}

‎regression/contracts/assigns_enforce_arrays_12/test.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+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when a function with an array assigns target
10+
calls a function which may assign below the allowable range.

‎regression/contracts/assigns_enforce_arrays_13/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void assigns_ptr(int *x) __CPROVER_assigns(*x)
2+
{
3+
*x = 200;
4+
}
5+
6+
/* clang-format off */
7+
void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
8+
/* clang-format on */
9+
{
10+
int *ptr = &(a[3]);
11+
assigns_ptr(ptr);
12+
}
13+
14+
int main()
15+
{
16+
int arr[10];
17+
assigns_range(arr, 10);
18+
19+
return 0;
20+
}

‎regression/contracts/assigns_enforce_arrays_13/test.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+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Checks whether verification succeeds when an array is assigned via a
10+
function call which assigns a pointer to one of its elements.

‎regression/contracts/assigns_enforce_arrays_14/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void assigns_ptr(int *x) __CPROVER_assigns(*x)
2+
{
3+
*x = 200;
4+
}
5+
6+
/* clang-format off */
7+
void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
8+
/* clang-format on */
9+
{
10+
int *ptr = &(a[7]);
11+
assigns_ptr(ptr);
12+
}
13+
14+
int main()
15+
{
16+
int arr[10];
17+
assigns_range(arr, 10);
18+
19+
return 0;
20+
}

‎regression/contracts/assigns_enforce_arrays_14/test.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+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Checks whether verification fails when an array is assigned via a
10+
function call which assigns a pointer to an element out of the
11+
allowable range.

0 commit comments

Comments
 (0)