Skip to content

Commit da879dc

Browse files
author
Remi Delmas
committed
fix test desc
1 parent c0c7808 commit da879dc

File tree

1 file changed

+1
-1
lines changed
  • regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail

1 file changed

+1
-1
lines changed

regression/contracts-dfcc/test_pointer_predicate_enforce_requires_in_range_equals_fail/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE dfcc-only
22
main.c
33
--dfcc main --enforce-contract foo
4-
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate: FAILURE$
4+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate: FAILURE$
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)