Skip to content

Commit dfed234

Browse files
author
Remi Delmas
committed
Fix line numbers in tests.
1 parent b069920 commit dfed234

File tree

3 files changed

+41
-41
lines changed
  • regression/contracts-dfcc
    • test_is_fresh_enforce_requires_disjunction_fail
    • test_is_fresh_enforce_requires_disjunction_pass
    • test_is_fresh_replace_ensures_disjunction_pass

3 files changed

+41
-41
lines changed

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

+7-7
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ main.c
55
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
66
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
77
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
8-
^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
9-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
10-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
11-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
12-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
13-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
14-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
8+
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: FAILURE$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: FAILURE$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: FAILURE$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: FAILURE$
13+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: FAILURE$
14+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: FAILURE$
1515
^EXIT=10$
1616
^SIGNAL=0$
1717
^VERIFICATION FAILED$

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

+17-17
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
CORE dfcc-only
22
main.c
33
--dfcc main --enforce-contract foo
4-
^\[foo.assertion.\d+\] line 13 assertion 0: FAILURE$
5-
^\[foo.assigns.\d+\] line 14 Check that \*x is assignable: SUCCESS$
6-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer NULL in \*x: SUCCESS$
7-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer invalid in \*x: SUCCESS$
8-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: dead object in \*x: SUCCESS$
10-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11-
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: invalid integer address in \*x: SUCCESS$
12-
^\[foo.assertion.\d+\] line 16 assertion 0: FAILURE$
13-
^\[foo.assertion.\d+\] line 17 assertion x == \(\(.*\)NULL\): SUCCESS$
14-
^\[foo.assigns.\d+\] line 18 Check that \*y is assignable: SUCCESS$
15-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer NULL in \*y: SUCCESS$
16-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer invalid in \*y: SUCCESS$
17-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: dead object in \*y: SUCCESS$
19-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20-
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: invalid integer address in \*y: SUCCESS$
4+
^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
5+
^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
6+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
13+
^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
15+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
2121
^EXIT=10$
2222
^SIGNAL=0$
2323
^VERIFICATION FAILED$

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

+17-17
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
CORE dfcc-only
22
main.c
33
--dfcc main --replace-call-with-contract foo
4-
^\[bar.assertion.\d+\] line 25 assertion 0: FAILURE$
5-
^\[bar.assigns.\d+\] line 26 Check that \*x is assignable: SUCCESS$
6-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer NULL in \*x: SUCCESS$
7-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer invalid in \*x: SUCCESS$
8-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: dead object in \*x: SUCCESS$
10-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11-
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: invalid integer address in \*x: SUCCESS$
12-
^\[bar.assertion.\d+\] line 28 assertion 0: FAILURE$
13-
^\[bar.assertion.\d+\] line 29 assertion x == \(\(.*\)NULL\): SUCCESS$
14-
^\[bar.assigns.\d+\] line 30 Check that \*y is assignable: SUCCESS$
15-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer NULL in \*y: SUCCESS$
16-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer invalid in \*y: SUCCESS$
17-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: dead object in \*y: SUCCESS$
19-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20-
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: invalid integer address in \*y: SUCCESS$
4+
^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
5+
^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
6+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
13+
^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
15+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
2121
^EXIT=10$
2222
^SIGNAL=0$
2323
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)