Skip to content

Commit

Permalink
Fix line numbers in tests.
Browse files Browse the repository at this point in the history
  • Loading branch information
Remi Delmas committed Jan 12, 2025
1 parent d84f254 commit f1c90c7
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 41 deletions.
14 changes: 7 additions & 7 deletions regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,13 +5,13 @@ main.c
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: FAILURE$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: FAILURE$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
34 changes: 17 additions & 17 deletions regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
CORE dfcc-only
main.c
--dfcc main --enforce-contract foo
^\[foo.assertion.\d+\] line 13 assertion 0: FAILURE$
^\[foo.assigns.\d+\] line 14 Check that \*x is assignable: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer NULL in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer invalid in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: deallocated dynamic object in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: dead object in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer outside object bounds in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: invalid integer address in \*x: SUCCESS$
^\[foo.assertion.\d+\] line 16 assertion 0: FAILURE$
^\[foo.assertion.\d+\] line 17 assertion x == \(\(.*\)NULL\): SUCCESS$
^\[foo.assigns.\d+\] line 18 Check that \*y is assignable: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer NULL in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer invalid in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: deallocated dynamic object in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: dead object in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer outside object bounds in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: invalid integer address in \*y: SUCCESS$
^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
34 changes: 17 additions & 17 deletions regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
CORE dfcc-only
main.c
--dfcc main --replace-call-with-contract foo
^\[bar.assertion.\d+\] line 25 assertion 0: FAILURE$
^\[bar.assigns.\d+\] line 26 Check that \*x is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer NULL in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer invalid in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: deallocated dynamic object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: dead object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer outside object bounds in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: invalid integer address in \*x: SUCCESS$
^\[bar.assertion.\d+\] line 28 assertion 0: FAILURE$
^\[bar.assertion.\d+\] line 29 assertion x == \(\(.*\)NULL\): SUCCESS$
^\[bar.assigns.\d+\] line 30 Check that \*y is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer NULL in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer invalid in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: deallocated dynamic object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: dead object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer outside object bounds in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: invalid integer address in \*y: SUCCESS$
^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down

0 comments on commit f1c90c7

Please sign in to comment.