diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index 12560af6f29..e40bdd895b1 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/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$ diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 7a3762c1a04..6dbeecb1feb 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/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(