Skip to content

CONTRACTS: Populate function name in source locations #7037

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 17, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/contracts/assigns_repeated_ignored/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--enforce-contract foo
^Ignored duplicate expression '\*x' in assigns clause spec at file main.c line \d+$
^Ignored duplicate expression '\*x' in assigns clause spec at file main.c line \d+ function .*$
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/assigns_validity_pointer_02/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract bar
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
Expand Down
18 changes: 18 additions & 0 deletions regression/contracts/embedded_contract_fail_01/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
typedef void (*fun_ptr_t)(int x);

void bar(int x)
{
return;
}

void foo(void (*fun_ptr)(int x) __CPROVER_requires(x != 0))
{
return;
}

void main()
{
fun_ptr_t fun_ptr = bar;
foo(fun_ptr);
return;
}
12 changes: 12 additions & 0 deletions regression/contracts/embedded_contract_fail_01/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c

^.*: Function contracts allowed only at top-level declarations. .*$
^PARSING ERROR$
^EXIT=(1|64)$
^SIGNAL=0$
--
--
Checks if function contracts can be attached to function pointers
(with non-empty parameter lists) in function parameters. This should
fail. Exit code 64 for Windows servers.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You don't need to include "Exit code 64 for Windows servers." in the description, the error code itself is self-explanatory.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I felt better reminding myself why there are two acceptable exit codes. I'd like to keep the comment unless the 1 and 64 pattern is super common.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The pattern is quite common as it appears in 118 test description, but there is no harm in leaving this reminder here as well.

18 changes: 18 additions & 0 deletions regression/contracts/embedded_contract_fail_02/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
typedef int (*fun_ptr_t)();

int bar()
{
return 1;
}

void foo(int (*fun_ptr)() __CPROVER_ensures(__CPROVER_return_value == 1))
{
return;
}

void main()
{
fun_ptr_t fun_ptr = bar;
foo(fun_ptr);
return;
}
12 changes: 12 additions & 0 deletions regression/contracts/embedded_contract_fail_02/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c

^.*: Function contracts allowed only at top-level declarations. .*$
^PARSING ERROR$
^EXIT=(1|64)$
^SIGNAL=0$
--
--
Checks if function contracts can be attached to function pointers
(with empty parameter lists) in function parameters. This should
fail. Exit code 64 for Windows servers.
2 changes: 1 addition & 1 deletion regression/contracts/function-calls-05/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[main.assertion.\d+\] line \d+ assertion foo\(\&x, \&y\) \=\= 10: SUCCESS
^VERIFICATION SUCCESSFUL$
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--replace-call-with-contract foo
^\[precondition.\d+] file main.c line 19 Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
^\[foo.precondition.\d+] line 19 Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/history-pointer-enforce-09/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
Expand Down
6 changes: 3 additions & 3 deletions regression/contracts/history-pointer-enforce-10/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ main.c
--enforce-contract foo --enforce-contract bar --enforce-contract baz
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[baz.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/history-pointer-replace-01/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ main.c
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
ASSERT \*\(address_of.*n.*\) > 0
ASSUME \*\(address_of.*n.*\) = tmp_cc[\$\d]? \+ 2
ASSUME \*\(address_of.*n.*\) = .*tmp_cc[\$\d]? \+ 2
--
--
Verification:
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/history-pointer-replace-02/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ main.c
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
ASSERT \*\(address_of.*n.*\) = 0
ASSUME \*\(address_of.*n.*\) ≥ tmp_cc[\$\d]? \+ 2
ASSUME \*\(address_of.*n.*\) ≥ .*tmp_cc[\$\d]? \+ 2
--
--
Verification:
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/history-pointer-replace-04/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=10$
^SIGNAL=0$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
^\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
^VERIFICATION FAILED$
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract f1
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract f1
^EXIT=0$
^SIGNAL=0$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract f1
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ main.c
--replace-call-with-contract f1 --replace-call-with-contract f2
^EXIT=10$
^SIGNAL=0$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE$
^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
^\[f2.precondition.\d+\] line \d+ Check requires clause: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract f1
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract f1
^EXIT=0$
^SIGNAL=0$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract f1
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract f1
^EXIT=0$
^SIGNAL=0$
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract f1
^EXIT=0$
^SIGNAL=0$
^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_aliasing_enforce/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_aliasing_ensure/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_aliasing_replace/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=10$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
^VERIFICATION FAILED$
--
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_array_memory_enforce/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_array_memory_replace/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=0$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
\[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
^VERIFICATION SUCCESSFUL$
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=10$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
^VERIFICATION FAILED$
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract sub_ptr_values
^EXIT=0$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
\[sub_ptr_values.precondition.\d+\] line \d+ Check requires clause: SUCCESS
^VERIFICATION SUCCESSFUL$
--
--
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_scalar_memory_enforce/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
^VERIFICATION SUCCESSFUL$
--
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_scalar_memory_replace/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=0$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
\[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS
\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_struct_enforce/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that x->qux is assignable: SUCCESS
\[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_struct_member_enforce/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--enforce-contract foo
^EXIT=0$
^SIGNAL=0$
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
\[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS
\[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/contracts/test_struct_replace/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--replace-call-with-contract foo
^EXIT=0$
^SIGNAL=0$
\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
\[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS
\[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS
^VERIFICATION SUCCESSFUL$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--apply-loop-contracts --replace-call-with-contract ackermann
^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
Expand Down
Loading