Skip to content

Commit dfe0d89

Browse files
committed
Revert "Add deprecation warning for intrinsic __CPROVER_allocated_memory in goto_check_c.cpp."
This reverts commit d6c19db.
1 parent bc3baf8 commit dfe0d89

File tree

1 file changed

+0
-11
lines changed

1 file changed

+0
-11
lines changed

src/ansi-c/goto_check_c.cpp

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff 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(

0 commit comments

Comments
 (0)