Populate function name in source locations for function contracts

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

Author: Nathan Wetzler

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,15 @@
+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,11 @@
+CORE
+main.c
+
+^Assertion failed: \(contract_in_global_scope || contract_in_top_level_function_scope\), function yyansi_cparse, file parser.y, line \d+.$
+^EXIT=134$
+^SIGNAL=0$
+--
+--
+Checks if function contracts can be attached to function pointers
+(with non-empty parameter lists) in function parameters.  This should
+fail.

regression/contracts/embedded_contract_fail_02/main.c

@@ -0,0 +1,15 @@
+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,11 @@
+CORE
+main.c
+
+^Assertion failed: \(contract_in_global_scope || contract_in_top_level_function_scope\), function yyansi_cparse, file parser.y, line \d+.$
+^EXIT=134$
+^SIGNAL=0$
+--
+--
+Checks if function contracts can be attached to function pointers
+(with empty parameter lists) in function parameters.  This should
+fail.

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