malloc breaks reasoning about assigns
ID0002455: This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002455 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-10-17 |
| Reporter | jwaksbaum | Assigned To | correnson | Resolution | suspended |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | i386 | OS | Darwin | OS Version | 18.6.0 |
| Product Version | Frama-C 18-Argon | Target Version | - | Fixed in Version | - |
Description :
If a function contains a call to malloc, WP fails to verify its assigns clause.
This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
Steps To Reproduce :
Verify a function with a call to malloc and assigns \nothing
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f
Verify a function with the same contract as malloc, which only calls malloc
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper