| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
| Issue History |
|||
| 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 |
| Issue History |