| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000041 | Frama-C | Plug-in > jessie | public | 2009-04-07 15:36 | 2009-06-23 18:03 | ||||
| Reporter | virgile | ||||||||
| Assigned To | cmarche | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Lithium-20081201 | ||||||||
| Target Version | Frama-C Beryllium-20090601-beta1 | Fixed in Version | Frama-C Beryllium-20090601-beta1 | ||||||
| Summary | 0000041: Inability to prove assigns clauses on simple array code | ||||||||
| Description | [bug 7560 from old bts, reported by David Mentré] Hello, With this code: ---- #include <string.h> #define MAX 12 int a[MAX]; char *c[MAX]; /*@ assigns a[..]; */ void assign_int(void) { int i; //@ loop invariant 0 <= i && i <= MAX; for (i = 0; i < MAX; i++) { a[i] = 0x45; } } /*@ assigns c[..]; */ void assign_char(void) { int i; //@ loop invariant 0 <= i && i <= MAX; for (i = 0; i < MAX; i++) { c[i] = strndup("something", MAX); } } /*@ assigns a[..]; assigns c[..]; */ void main(void) { assign_int(); assign_char(); } ------ On this code, I cannot prove properties "assigns a[..];" for assign_int() and "assigns c[..];" for assign_char(). However the assignation seems obvious to me. I have tried "assigns a[0..11];" without success. Is assigns broken? Boris had a similar issue: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/000487.html Yours, d. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
| There are no notes attached to this issue. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2009-04-07 15:36 | virgile | New Issue | |
| 2009-04-07 15:40 | signoles | Status | new => acknowledged |
| 2009-04-30 16:48 | monate | Status | acknowledged => assigned |
| 2009-04-30 16:48 | monate | Assigned To | => cmarche |
| 2009-06-04 15:16 | cmarche | Target Version | => Frama-C Beryllium |
| 2009-06-18 13:41 | cmarche | Resolution | open => fixed |
| 2009-06-18 13:42 | cmarche | Status | assigned => resolved |
| 2009-06-23 18:02 | signoles | Status | resolved => closed |
| 2009-06-23 18:03 | signoles | Fixed in Version | => Frama-C Beryllium beta-1 |
| Issue History |