Merge pull request #6876 from NlightNFotis/warn_allocated_memory_depracated

Add deprecation warning for intrinsic `__CPROVER_allocated_memory`

Author: NlightNFotis

regression/cbmc/memory_allocation1/test.desc

@@ -3,6 +3,7 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
+^\*\*\*\* WARNING: `__CPROVER_allocated_memory' in file main\.c line \d+ function main$
 ^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
 ^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
 ^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$

src/ansi-c/goto_check_c.cpp

@@ -436,6 +436,17 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
           "allocated_memory")
         continue;
 
+      const auto function_line = function.source_location().as_string();
+      log.warning() << "**** WARNING: `" CPROVER_PREFIX "allocated_memory' in "
+                    << function_line << messaget::eom;
+      log.warning() << "**** WARNING: `" CPROVER_PREFIX
+                       "allocated_memory' is "
+                       "deprecated and scheduled for deletion "
+                    << "in version 6 and upwards." << messaget::eom;
+      log.warning() << "Please avoid using this intrinsic. For more "
+                       "information, please check issue "
+                    << "cbmc#6872 in Github" << messaget::eom;
+
       const code_function_callt::argumentst &args =
         instruction.call_arguments();
       if(