__CPROVER_return_value in postcondtions

Author: kroening

regression/cprover/contracts/recursive_function2.desc

@@ -1,7 +1,7 @@
-KNOWNBUG
+CORE
 recursive_function2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[recursive_function\.precondition\.1] line \d+ postcondition recursive_function: SUCCESS$
+^\[recursive_function\.postcondition\.1] line \d+ postcondition: SUCCESS$
 --

src/cprover/instrument_contracts.cpp

@@ -283,6 +283,11 @@ void replace_function_calls_by_contracts(
           replace_symbol.insert(p_symbol, arguments[p]);
         }
 
+        // replace __CPROVER_return_value by the lhs of the call
+        const auto &call_lhs = it->call_lhs();
+        replace_symbol.insert(
+          symbol_exprt("__CPROVER_return_value", call_lhs.type()), call_lhs);
+
         for(auto &precondition : contract.requires())
         {
           auto location = it->source_location();