Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
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. | ||||
Relationships | |||||
Attached Files | ![]() https://bts.frama-c.com/file_download.php?file_id=1331&type=bug |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
||||
|
|||||
|
|
Issue History | |||||
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 | bug_revision_view_page.php?bugnote_id=6914#r433 | ||
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 | bug_revision_view_page.php?bugnote_id=6915#r435 | ||
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 |