Code contracts: add source location to function pointer contracts

The expression constructed in the parser never got a source location
assigned, yet it was this sub-expression that was actually retained by
type checking. Consequently, properties were printed without a source
location.

Author: tautschnig

regression/contracts/function-pointer-contracts-replace/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --replace-call-with-contract foo
-^\[precondition.\d+] Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
+^\[precondition.\d+] file main.c 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$

src/ansi-c/parser.y

@@ -3303,6 +3303,7 @@ cprover_function_contract:
           exprt tmp(ID_function_pointer_obeys_contract);
           tmp.add_to_operands(std::move(parser_stack($3)));
           tmp.add_to_operands(std::move(parser_stack($5)));
+          tmp.add_source_location()=parser_stack($$).source_location();
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')'
@@ -3312,6 +3313,7 @@ cprover_function_contract:
           exprt tmp(ID_function_pointer_obeys_contract);
           tmp.add_to_operands(std::move(parser_stack($3)));
           tmp.add_to_operands(std::move(parser_stack($5)));
+          tmp.add_source_location()=parser_stack($$).source_location();
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | cprover_contract_assigns