File tree Expand file tree Collapse file tree 1 file changed +0
-11
lines changed
Expand file tree Collapse file tree 1 file changed +0
-11
lines changed Original file line number Diff line number Diff line change @@ -441,17 +441,6 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
441441 " allocated_memory" )
442442 continue ;
443443
444- const auto function_line = function.source_location ().as_string ();
445- log.warning () << " **** WARNING: `" CPROVER_PREFIX " allocated_memory' in "
446- << function_line << messaget::eom;
447- log.warning () << " **** WARNING: `" CPROVER_PREFIX
448- " allocated_memory' is "
449- " deprecated and scheduled for deletion "
450- << " in version 6 and upwards." << messaget::eom;
451- log.warning () << " Please avoid using this intrinsic. For more "
452- " information, please check issue "
453- << " cbmc#6872 in Github" << messaget::eom;
454-
455444 const code_function_callt::argumentst &args =
456445 instruction.call_arguments ();
457446 if (
You can’t perform that action at this time.
0 commit comments