Merge pull request #7037 from nwetzler/contract-coverage

CONTRACTS: Populate function name in source locations

Author: jimgrundy

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$

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$

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$

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;
+}

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.

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;
+}

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.

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$
 --

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$

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$
 --

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$

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:

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:

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$
 --

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

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

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

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

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

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

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$
 --

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

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

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

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

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$

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$
 --

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

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$

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$
 --

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$
 --
 --

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$
 --

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$

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

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$

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$

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$