Skip to content

Commit 8a32d75

Browse files
author
Remi Delmas
committed
Add tests for assumption uniqueness checking
1 parent 2d5a8b2 commit 8a32d75

File tree

24 files changed

+377
-0
lines changed
  • regression/contracts-dfcc
    • test_pointer_predicate_enforce_requires_equals_equals_fail
    • test_pointer_predicate_enforce_requires_equals_equals_pass
    • test_pointer_predicate_enforce_requires_in_range_equals_fail
    • test_pointer_predicate_enforce_requires_in_range_equals_pass
    • test_pointer_predicate_enforce_requires_in_range_in_range_pass
    • test_pointer_predicate_enforce_requires_is_fresh_equals_fail
    • test_pointer_predicate_enforce_requires_is_fresh_equals_pass
    • test_pointer_predicate_enforce_requires_is_fresh_in_range_fail
    • test_pointer_predicate_enforce_requires_is_fresh_in_range_pass
    • test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail
    • test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass
    • test_pointer_predicate_requires_in_range_in_range_fail

24 files changed

+377
-0
lines changed

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_pointer_equals(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_pointer_equals(y, x) || __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_equals_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_equals(y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_equals(y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_in_range_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) && __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(__CPROVER_is_fresh(y, sizeof(int)) || __CPROVER_pointer_equals(y, x))
6+
__CPROVER_assigns(*y)
7+
__CPROVER_ensures(*y == 1)
8+
__CPROVER_ensures(*x == 1 || *x == 0)
9+
// clang-format on
10+
{
11+
*y = 1;
12+
}
13+
14+
int main()
15+
{
16+
int *x;
17+
int *y;
18+
foo(x, y);
19+
return 0;
20+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_equals_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_is_fresh(y, sizeof(int)) &&
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1 || *x == 0)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(x[SIZE-1] == 0)
6+
__CPROVER_requires(
7+
__CPROVER_is_fresh(y, sizeof(int)) ||
8+
__CPROVER_pointer_in_range_dfcc(x, y, x))
9+
__CPROVER_assigns(*y)
10+
__CPROVER_ensures(*y == 1)
11+
__CPROVER_ensures(*x == 1 || *x == 0)
12+
// clang-format on
13+
{
14+
*y = 1;
15+
}
16+
17+
int main()
18+
{
19+
int *x;
20+
int *y;
21+
foo(x, y);
22+
return 0;
23+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_in_range_pass/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/main.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
void foo(int *x)
2+
// clang-format off
3+
__CPROVER_requires(
4+
__CPROVER_is_fresh(x, sizeof(int)) && __CPROVER_is_fresh(x, sizeof(int)))
5+
__CPROVER_assigns(*x)
6+
__CPROVER_ensures(*x == 0)
7+
// clang-format on
8+
{
9+
*x = 0;
10+
}
11+
12+
int main()
13+
{
14+
int *x;
15+
foo(x);
16+
return 0;
17+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_fail/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other predicate: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
Tests that assuming the more than one pointer predicate on the same target pointer
11+
at the same time triggers a failure.

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/main.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
void foo(int *x)
2+
// clang-format off
3+
__CPROVER_requires(
4+
__CPROVER_is_fresh(x, sizeof(int)) || __CPROVER_is_fresh(x, sizeof(int)))
5+
__CPROVER_assigns(*x)
6+
__CPROVER_ensures(*x == 0)
7+
// clang-format on
8+
{
9+
*x = 0;
10+
}
11+
12+
int main()
13+
{
14+
int *x;
15+
foo(x);
16+
return 0;
17+
}

‎regression/contracts-dfcc/test_pointer_predicate_enforce_requires_is_fresh_is_fresh_pass/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFULL$
7+
--
8+
--
9+
Tests that a same pointer can be the target of multiple pointer predicates as
10+
long as they do not apply at the same time.
11+
- `x` is fresh and inialized to 0
12+
- `y` is equal to `x`if select is true, or fresh otherwise
13+
- foo assigns y to 1
14+
- x is equal to 1 if select is true, 0 otherwise

‎regression/contracts-dfcc/test_pointer_predicate_requires_in_range_in_range_fail/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(*x == 0)
5+
__CPROVER_requires(
6+
__CPROVER_pointer_in_range_dfcc(x, y, x) &&
7+
__CPROVER_pointer_in_range_dfcc(x, y, x))
8+
__CPROVER_assigns(*y)
9+
__CPROVER_ensures(*y == 1)
10+
__CPROVER_ensures(*x == 1)
11+
// clang-format on
12+
{
13+
*y = 1;
14+
}
15+
16+
int main()
17+
{
18+
int *x;
19+
int *y;
20+
foo(x, y);
21+
return 0;
22+
}

0 commit comments

Comments
 (0)