View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002126 | Frama-C | Plug-in > wp | public | 2015-06-02 08:52 | 2016-01-26 08:43 | ||||
Reporter | virgile | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Magnesium | |||||||
Summary | 0002126: WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml) | ||||||||
Description | On the example source below, frama-c -wp reduced.i crashes with the following error: File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine). -- reduced.i /*@ assigns *(p1); */ int fn1(char *p1); /*@ assigns \nothing; */ void fn2(void) { char pcr_index; fn1(&pcr_index); } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-06-02 08:52 | virgile | New Issue | |
2015-06-02 08:52 | virgile | Status | new => assigned |
2015-06-02 08:52 | virgile | Assigned To | => correnson |
2015-06-29 16:42 | correnson | Note Added: 0005951 | |
2015-06-29 16:42 | correnson | Status | assigned => resolved |
2015-06-29 16:42 | correnson | Fixed in Version | => Frama-C Magnesium |
2015-06-29 16:42 | correnson | Resolution | open => fixed |
2016-01-26 08:43 | signoles | Status | resolved => closed |