File tree Expand file tree Collapse file tree 2 files changed +0
-12
lines changed
regression/cbmc/memory_allocation1 Expand file tree Collapse file tree 2 files changed +0
-12
lines changed Original file line number Diff line number Diff line change 3
3
--pointer-check
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
- ^\*\*\*\* WARNING: `__CPROVER_allocated_memory' in file main\.c line \d+ function main$
7
6
^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
8
7
^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
9
8
^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$
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)
441
441
" allocated_memory" )
442
442
continue ;
443
443
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
-
455
444
const code_function_callt::argumentst &args =
456
445
instruction.call_arguments ();
457
446
if (
You can’t perform that action at this time.
0 commit comments