| 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 | |
| Platform | | OS | | OS Version | |
| 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
#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