WP warning not clear
ID0002482: This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002482 | Frama-C | Plug-in > wp | public | 2019-10-22 | 2020-02-17 |
| Reporter | jens | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Linux, macOS | OS Version | - |
| Product Version | Frama-C 19-Potassium | Target Version | - | Fixed in Version | Frama-C 20-Calcium |
Description :
When I run frama-c -wp -wp-rte -wp-model Typed f.c on the attached file, I obtain the warning
[wp] Warning: Memory model hypotheses for function 'f': /*@ behavior typed: requires \separated(p+(..),a); */ void f(int *a);
However, when I add this requirement by removing the corresponding comment in the contract, then the warning still occurs.
What can I do to make this warning disappear?