From 83abf73a541646fa855888a0050de1eb7cae2ea4 Mon Sep 17 00:00:00 2001 From: Nathan Wetzler Date: Fri, 12 Aug 2022 18:51:08 -0500 Subject: [PATCH] CONTRACTS: Populate function name in source locations During parsing of function parameters, the function name should be set in the source location, but only for top-level function declarations and definitions. In addition, function contracts should be only allowed for top-level function declarations and definitions. CBMC Viewer reports a failure when analyzing the incomplete coverage report, causing the CMBC Starter Kit to fail during a standard build. Also removed source location from "end function" command during contract checking and added proper source location to function contract instrumentation. Resolves issues #7032, #7070 --- .../assigns_repeated_ignored/test.desc | 2 +- .../assigns_validity_pointer_02/test.desc | 2 +- .../test.desc | 2 +- .../embedded_contract_fail_01/main.c | 18 +++++++ .../embedded_contract_fail_01/test.desc | 12 +++++ .../embedded_contract_fail_02/main.c | 18 +++++++ .../embedded_contract_fail_02/test.desc | 12 +++++ .../contracts/function-calls-05/test.desc | 2 +- .../test.desc | 2 +- .../history-pointer-enforce-09/test.desc | 2 +- .../history-pointer-enforce-10/test.desc | 6 +-- .../history-pointer-replace-01/test.desc | 2 +- .../history-pointer-replace-02/test.desc | 2 +- .../history-pointer-replace-04/test.desc | 2 +- .../quantifiers-exists-both-enforce/test.desc | 2 +- .../quantifiers-exists-both-replace/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 4 +- .../quantifiers-forall-both-enforce/test.desc | 2 +- .../quantifiers-forall-both-replace/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../contracts/test_aliasing_enforce/test.desc | 2 +- .../contracts/test_aliasing_ensure/test.desc | 2 +- .../test_aliasing_ensure_indirect/test.desc | 2 +- .../contracts/test_aliasing_replace/test.desc | 2 +- .../test_array_memory_enforce/test.desc | 2 +- .../test_array_memory_replace/test.desc | 2 +- .../test.desc | 2 +- .../test_possibly_aliased_arguments/test.desc | 2 +- .../test_scalar_memory_enforce/test.desc | 2 +- .../test_scalar_memory_replace/test.desc | 2 +- .../contracts/test_struct_enforce/test.desc | 2 +- .../test_struct_member_enforce/test.desc | 2 +- .../contracts/test_struct_replace/test.desc | 2 +- .../test.desc | 4 +- src/ansi-c/parser.y | 47 ++++++++++++++++++- src/goto-instrument/contracts/contracts.cpp | 11 ++--- 39 files changed, 148 insertions(+), 44 deletions(-) create mode 100644 regression/contracts/embedded_contract_fail_01/main.c create mode 100644 regression/contracts/embedded_contract_fail_01/test.desc create mode 100644 regression/contracts/embedded_contract_fail_02/main.c create mode 100644 regression/contracts/embedded_contract_fail_02/test.desc diff --git a/regression/contracts/assigns_repeated_ignored/test.desc b/regression/contracts/assigns_repeated_ignored/test.desc index 7e8ecdffd98..2302efd7ec3 100644 --- a/regression/contracts/assigns_repeated_ignored/test.desc +++ b/regression/contracts/assigns_repeated_ignored/test.desc @@ -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$ diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index c918ef2ee61..0cbf7a50e52 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -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$ diff --git a/regression/contracts/contracts_with_function_pointers/test.desc b/regression/contracts/contracts_with_function_pointers/test.desc index 480b8532f47..1520b8dba51 100644 --- a/regression/contracts/contracts_with_function_pointers/test.desc +++ b/regression/contracts/contracts_with_function_pointers/test.desc @@ -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$ diff --git a/regression/contracts/embedded_contract_fail_01/main.c b/regression/contracts/embedded_contract_fail_01/main.c new file mode 100644 index 00000000000..00b38ce7e21 --- /dev/null +++ b/regression/contracts/embedded_contract_fail_01/main.c @@ -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; +} diff --git a/regression/contracts/embedded_contract_fail_01/test.desc b/regression/contracts/embedded_contract_fail_01/test.desc new file mode 100644 index 00000000000..0feff02cf54 --- /dev/null +++ b/regression/contracts/embedded_contract_fail_01/test.desc @@ -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. diff --git a/regression/contracts/embedded_contract_fail_02/main.c b/regression/contracts/embedded_contract_fail_02/main.c new file mode 100644 index 00000000000..bdd0a1bd645 --- /dev/null +++ b/regression/contracts/embedded_contract_fail_02/main.c @@ -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; +} diff --git a/regression/contracts/embedded_contract_fail_02/test.desc b/regression/contracts/embedded_contract_fail_02/test.desc new file mode 100644 index 00000000000..440129b001a --- /dev/null +++ b/regression/contracts/embedded_contract_fail_02/test.desc @@ -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. diff --git a/regression/contracts/function-calls-05/test.desc b/regression/contracts/function-calls-05/test.desc index a4132a04b30..431b7072620 100644 --- a/regression/contracts/function-calls-05/test.desc +++ b/regression/contracts/function-calls-05/test.desc @@ -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$ -- diff --git a/regression/contracts/function-pointer-contracts-replace/test.desc b/regression/contracts/function-pointer-contracts-replace/test.desc index a9495d7333e..81dab427a53 100644 --- a/regression/contracts/function-pointer-contracts-replace/test.desc +++ b/regression/contracts/function-pointer-contracts-replace/test.desc @@ -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$ diff --git a/regression/contracts/history-pointer-enforce-09/test.desc b/regression/contracts/history-pointer-enforce-09/test.desc index 226c63e735e..4cf2a84e871 100644 --- a/regression/contracts/history-pointer-enforce-09/test.desc +++ b/regression/contracts/history-pointer-enforce-09/test.desc @@ -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$ -- diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index afbbf3e463c..6ab7a0823ef 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -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$ diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc index d4ed769e2b5..db905317853 100644 --- a/regression/contracts/history-pointer-replace-01/test.desc +++ b/regression/contracts/history-pointer-replace-01/test.desc @@ -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: diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc index 10010d78476..074857ec25c 100644 --- a/regression/contracts/history-pointer-replace-02/test.desc +++ b/regression/contracts/history-pointer-replace-02/test.desc @@ -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: diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc index 6b62750371c..bf0590f9044 100644 --- a/regression/contracts/history-pointer-replace-04/test.desc +++ b/regression/contracts/history-pointer-replace-04/test.desc @@ -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$ -- diff --git a/regression/contracts/quantifiers-exists-both-enforce/test.desc b/regression/contracts/quantifiers-exists-both-enforce/test.desc index 7192b974a7a..644f4800596 100644 --- a/regression/contracts/quantifiers-exists-both-enforce/test.desc +++ b/regression/contracts/quantifiers-exists-both-enforce/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-exists-both-replace/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc index c67a81fea6c..2aa54a4e3ec 100644 --- a/regression/contracts/quantifiers-exists-both-replace/test.desc +++ b/regression/contracts/quantifiers-exists-both-replace/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-exists-requires-enforce/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc index adc9e03e0c6..a7e28e739cb 100644 --- a/regression/contracts/quantifiers-exists-requires-enforce/test.desc +++ b/regression/contracts/quantifiers-exists-requires-enforce/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-exists-requires-replace/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc index bfc06261fd9..65664ebb47b 100644 --- a/regression/contracts/quantifiers-exists-requires-replace/test.desc +++ b/regression/contracts/quantifiers-exists-requires-replace/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-forall-both-enforce/test.desc b/regression/contracts/quantifiers-forall-both-enforce/test.desc index 5119ffa76ac..dcd56763a56 100644 --- a/regression/contracts/quantifiers-forall-both-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-both-enforce/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-forall-both-replace/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc index f075906b014..b59b1547723 100644 --- a/regression/contracts/quantifiers-forall-both-replace/test.desc +++ b/regression/contracts/quantifiers-forall-both-replace/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index 43d5442d71d..ebd37152ecf 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -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$ -- diff --git a/regression/contracts/quantifiers-forall-requires-enforce/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc index 8f1622ddf16..23f9c2209e1 100644 --- a/regression/contracts/quantifiers-forall-requires-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-requires-enforce/test.desc @@ -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 diff --git a/regression/contracts/quantifiers-forall-requires-replace/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc index 82a89f03811..89df08c7c91 100644 --- a/regression/contracts/quantifiers-forall-requires-replace/test.desc +++ b/regression/contracts/quantifiers-forall-requires-replace/test.desc @@ -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 diff --git a/regression/contracts/test_aliasing_enforce/test.desc b/regression/contracts/test_aliasing_enforce/test.desc index 93495129f1b..f26bda8c1f1 100644 --- a/regression/contracts/test_aliasing_enforce/test.desc +++ b/regression/contracts/test_aliasing_enforce/test.desc @@ -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 diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc index c7fcc2e0264..70ae1bdd9ff 100644 --- a/regression/contracts/test_aliasing_ensure/test.desc +++ b/regression/contracts/test_aliasing_ensure/test.desc @@ -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 diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 95b62b742fe..226a5d2aebb 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -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$ diff --git a/regression/contracts/test_aliasing_replace/test.desc b/regression/contracts/test_aliasing_replace/test.desc index 17c49800001..253ab0ece76 100644 --- a/regression/contracts/test_aliasing_replace/test.desc +++ b/regression/contracts/test_aliasing_replace/test.desc @@ -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$ -- diff --git a/regression/contracts/test_array_memory_enforce/test.desc b/regression/contracts/test_array_memory_enforce/test.desc index 169bc8f4b86..6dd73084d7d 100644 --- a/regression/contracts/test_array_memory_enforce/test.desc +++ b/regression/contracts/test_array_memory_enforce/test.desc @@ -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 diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc index 201a79d1f1b..d759b56790e 100644 --- a/regression/contracts/test_array_memory_replace/test.desc +++ b/regression/contracts/test_array_memory_replace/test.desc @@ -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$ diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc index 0736db61794..98077b6e52e 100644 --- a/regression/contracts/test_array_memory_too_small_replace/test.desc +++ b/regression/contracts/test_array_memory_too_small_replace/test.desc @@ -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$ -- diff --git a/regression/contracts/test_possibly_aliased_arguments/test.desc b/regression/contracts/test_possibly_aliased_arguments/test.desc index 37292fb85d9..ca62c45ef63 100644 --- a/regression/contracts/test_possibly_aliased_arguments/test.desc +++ b/regression/contracts/test_possibly_aliased_arguments/test.desc @@ -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$ -- -- diff --git a/regression/contracts/test_scalar_memory_enforce/test.desc b/regression/contracts/test_scalar_memory_enforce/test.desc index 3a8aa7f3a99..f32b3905b98 100644 --- a/regression/contracts/test_scalar_memory_enforce/test.desc +++ b/regression/contracts/test_scalar_memory_enforce/test.desc @@ -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$ -- diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc index 67092f9ddf3..2e546d4c0fd 100644 --- a/regression/contracts/test_scalar_memory_replace/test.desc +++ b/regression/contracts/test_scalar_memory_replace/test.desc @@ -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$ diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc index 74700a3258c..b2b0799d18e 100644 --- a/regression/contracts/test_struct_enforce/test.desc +++ b/regression/contracts/test_struct_enforce/test.desc @@ -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 diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc index 7f7a8adf160..82c4b78f740 100644 --- a/regression/contracts/test_struct_member_enforce/test.desc +++ b/regression/contracts/test_struct_member_enforce/test.desc @@ -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$ diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc index 0553e58cd78..7d39f3e1b27 100644 --- a/regression/contracts/test_struct_replace/test.desc +++ b/regression/contracts/test_struct_replace/test.desc @@ -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$ diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc index ae2ba7900c4..66f44754dda 100644 --- a/regression/contracts/variant_multidimensional_ackermann/test.desc +++ b/regression/contracts/variant_multidimensional_ackermann/test.desc @@ -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$ diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 4790ee07d09..9941c9e7184 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -3407,6 +3407,19 @@ cprover_function_contract_sequence_opt: /* nothing */ { init($$); } | cprover_function_contract_sequence + { + // Function contracts should either be attached to a + // top-level function declaration or top-level function + // definition. Any embedded function pointer scopes should + // be disallowed. + int contract_in_global_scope = (PARSER.scopes.size() == 1); + int contract_in_top_level_function_scope = (PARSER.scopes.size() == 2); + if(!contract_in_global_scope && !contract_in_top_level_function_scope) + { + yyansi_cerror("Function contracts allowed only at top-level declarations."); + YYABORT; + } + } ; postfixing_abstract_declarator: @@ -3447,15 +3460,41 @@ postfixing_abstract_declarator: parameter_postfixing_abstract_declarator: array_abstract_declarator | '(' ')' + { + // Set function name (last declarator) in source location + // before parsing function contracts. Only do this if we + // are at a global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(PARSER.current_scope().last_declarator); + } + // Use last declarator (i.e., function name) to name + // the scope. + PARSER.new_scope( + id2string(PARSER.current_scope().last_declarator)+"::"); + } cprover_function_contract_sequence_opt { set($1, ID_code); stack_type($1).add(ID_parameters); stack_type($1).subtype()=typet(ID_abstract); - $$ = merge($3, $1); + PARSER.pop_scope(); + + // Clear function name in source location after parsing if + // at global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(irep_idt()); + } + + $$ = merge($4, $1); } | '(' { + // Set function name (last declarator) in source location + // before parsing function contracts. Only do this if we + // are at a global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(PARSER.current_scope().last_declarator); + } // Use last declarator (i.e., function name) to name // the scope. PARSER.new_scope( @@ -3472,6 +3511,12 @@ parameter_postfixing_abstract_declarator: swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes())); PARSER.pop_scope(); + // Clear function name in source location after parsing if + // at global scope. + if (PARSER.current_scope().prefix.empty()) { + PARSER.set_function(irep_idt()); + } + if(parser_stack($5).is_not_nil()) { adjust_KnR_parameters(parser_stack($$).add(ID_parameters), parser_stack($5)); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index c3fb7fc9bc1..84ae4cc4a17 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1382,15 +1382,12 @@ void code_contractst::enforce_contract(const irep_idt &function) goto_functions.function_map.erase(old_function); // Place a new symbol with the mangled name into the symbol table - source_locationt sl; - sl.set_file("instrumented for code contracts"); - sl.set_line("0"); symbolt mangled_sym; const symbolt *original_sym = symbol_table.lookup(original); mangled_sym = *original_sym; mangled_sym.name = mangled; mangled_sym.base_name = mangled; - mangled_sym.location = sl; + mangled_sym.location = original_sym->location; const auto mangled_found = symbol_table.insert(std::move(mangled_sym)); INVARIANT( mangled_found.second, @@ -1414,7 +1411,7 @@ void code_contractst::enforce_contract(const irep_idt &function) goto_functiont &wrapper = goto_functions.function_map[original]; wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers; - wrapper.body.add(goto_programt::make_end_function(sl)); + wrapper.body.add(goto_programt::make_end_function()); add_contract_check(original, mangled, wrapper.body); } @@ -1485,7 +1482,9 @@ void code_contractst::add_contract_check( // with expressions from the call site (e.g. the return value). exprt::operandst instantiation_values; - const auto &source_location = function_symbol.location; + source_locationt source_location = function_symbol.location; + // Set function in source location to original function + source_location.set_function(wrapper_function); // decl ret optionalt return_stmt;