View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002482 | Frama-C | Plug-in > wp | public | 2019-10-22 19:47 | 2020-02-17 18:08 | ||||
Reporter | jens | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | no change required | ||||||
Platform | OS | Linux, macOS | OS Version | ||||||
Product Version | Frama-C 19-Potassium | ||||||||
Target Version | Fixed in Version | Frama-C 20-Calcium | |||||||
Summary | 0002482: WP warning not clear | ||||||||
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? | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
correnson (manager) 2019-10-22 23:30 Last edited: 2019-10-22 23:32 |
These warnings are emitted because WP is not able to verify them on its own since it assumes these assumptions (or something weaker) to proceed. If you are confident that such requirements are still valid, you can turn off their emission with option -wp-(no)-warn-memory-model. Roadmap: in the future « Region » memory model, such hypotheses would be checked by WP on its own. |
correnson (manager) 2019-10-22 23:34 Last edited: 2019-10-22 23:35 |
Side note: some requirements are too strong as they are printed. For instance, you can see a requirement like « \valid(a + (..)) » although maybe it is sufficient to have « \valid(a + (0..n)) » for some well-chosen « n ». The same for separation hypotheses. This is why we do not add them to preconditions automatically. |
signoles (manager) 2020-02-17 18:08 |
Fixed in Frama-C 20.0 (Calcium). |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2019-10-22 19:47 | jens | New Issue | |
2019-10-22 19:47 | jens | Status | new => assigned |
2019-10-22 19:47 | jens | Assigned To | => correnson |
2019-10-22 19:47 | jens | File Added: f.c | |
2019-10-22 23:30 | correnson | Note Added: 0006914 | |
2019-10-22 23:32 | correnson | Note Edited: 0006914 | View Revisions |
2019-10-22 23:32 | correnson | Status | assigned => resolved |
2019-10-22 23:32 | correnson | Resolution | open => no change required |
2019-10-22 23:34 | correnson | Note Added: 0006915 | |
2019-10-22 23:35 | correnson | Note Edited: 0006915 | View Revisions |
2020-02-17 18:06 | signoles | Fixed in Version | => Frama-C 20-Calcium |
2020-02-17 18:08 | signoles | Status | resolved => closed |
2020-02-17 18:08 | signoles | Note Added: 0006939 |