Remove __CPROVER_allocated_memory from mman modelling #7773
Description
CBMC version: 5.85.0 (cbmc-5.85.0)
Operating system: N/A
Exact command line resulting in the issue: N/A
What behaviour did you expect: A model of mmap without __CPROVER_allocated_memory. It has been reported to be deprecated. Whenever it's used, CBMC prints the following message
**** WARNING: `__CPROVER_allocated_memory' is deprecated and scheduled for deletion in version 6 and upwards.
Please avoid using this intrinsic. For more information, please check issue cbmc#6872 in Github
What happened instead: Consider the following program.
// mmap.c
void * mmap(void *addr, __CPROVER_size_t length, signed int prot, signed int flags, signed int fd, long int offset);
void main(void)
{
int var_0;
unsigned int var_1;
void *var_2;
void *var_3;
unsigned int *var_4;
int var_5;
bb0:
;
var_1 = 16777215;
var_4 = &var_1;
var_3 = (void*) &var_1;
var_5 = 1 | 2;
var_2= mmap(var_3, 1024, var_5, 1, -1, 0);
bb1:
;
assert(var_2 != 0);
}If I invoke CBMC using the following command
goto-cc mmap.c -o mmap.o && goto-instrument mmap.o --add-library --generate-function-body-options assert-false-assume-false --generate-function-body '.*' --drop-unused-functions mmap.out && cbmc mmap.out
I get the following message
Reading GOTO program from 'mmap.o'
Adding CPROVER library (x86_64)
generate function bodies: matched function '__CPROVER_was_freed' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_object_from' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_assignable' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_is_freeable' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_object_upto' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_object_whole' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_freeable' begins with __CPROVER the generated body for this function may interfere with analysis
generate function bodies: matched function '__CPROVER_allocated_memory' begins with __CPROVER the generated body for this function may interfere with analysis
**** WARNING: `__CPROVER_allocated_memory' in file <builtin-library-mmap> line 46 function mmap
**** WARNING: `__CPROVER_allocated_memory' is deprecated and scheduled for deletion in version 6 and upwards.
Please avoid using this intrinsic. For more information, please check issue cbmc#6872 in Github
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Removing unused functions
Dropping 8 of 13 functions (5 used)
Writing GOTO program to 'mmap.out'
CBMC version 5.85.0 (cbmc-5.73.0-677-gb1d78e2e37) 64-bit x86_64 linux
Reading GOTO program from file mmap.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
**** WARNING: `__CPROVER_allocated_memory' in file <builtin-library-mmap> line 46 function mmap
**** WARNING: `__CPROVER_allocated_memory' is deprecated and scheduled for deletion in version 6 and upwards.
Please avoid using this intrinsic. For more information, please check issue cbmc#6872 in Github
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
aborting path on assume(false) at file <builtin-architecture-strings> line 20 function __CPROVER_allocated_memory thread 0
Runtime Symex: 0.00129843s
size of program expression: 58 steps
simple slicing removed 6 assignments
Generated 2 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.2979e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00206747s
Running propositional reduction
Post-processing
Runtime Post-process: 5.107e-06s
Solving with CaDiCaL sc2021
8679 variables, 138 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000505271s
Runtime decision procedure: 0.00261511s
** Results:
<builtin-architecture-strings> function __CPROVER_allocated_memory
[__CPROVER_allocated_memory.assertion.1] line 20 undefined function should be unreachable: FAILURE
mmap.c function main
[main.assertion.1] line 22 assertion var_2 != NULL: SUCCESS
** 1 of 2 failed (2 iterations)
VERIFICATION FAILED