Inability to prove assigns clauses on simple array code
ID0000041:
**This issue was created automatically from Mantis Issue 41. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000041 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **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 |
### 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.
issue