From bc3baf838d8cb5e1a535a93988c79ea14ab3a9f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 Sep 2023 12:27:54 +0000 Subject: [PATCH 1/2] Revert "Add a pattern to match deprecation warning in memory_allocation1.desc" This reverts commit ece1a848debdde6f325421c8aee7ad45c17f786a. --- regression/cbmc/memory_allocation1/test.desc | 1 - 1 file changed, 1 deletion(-) diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index b73d07f0f88..663bbf6176b 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -3,7 +3,6 @@ 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$ From dfe0d89137fdf2947f865dfe1845e6fafe3ad5ad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 Sep 2023 12:28:02 +0000 Subject: [PATCH 2/2] Revert "Add deprecation warning for intrinsic `__CPROVER_allocated_memory` in `goto_check_c.cpp`." This reverts commit d6c19db6197313d856886807e581cec51dbdb82f. --- src/ansi-c/goto_check_c.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 26e437195b9..330a6ae3517 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -441,17 +441,6 @@ 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(