--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] valid range of arrays within structures



I have a lot of code where arrays are kept in structures  here's a trivial
case:
struct SS{
int b;
int a[3];
};

struct SS xx;
int main(int argc, char *argv[]) {
int i = 0;
 xx.b = 8;
for (i=0; i < 3; i++) { xx.a[i] = i;}
}

Note xx is a global variable.

In doing the verification,  tried to place before  the loop
 the assertion :

/*@ assert \valid_range(xx.a,0,2); */

if a were not in the structure most if not all of the tools would prove this

but none of the tools seemed to get  it with a inside a structure. I also
tried using
using a type invariant

/*@ type invariant vrng(struct SS *s) = \valid(s->a+(0..2)); */

to no avail. Any help would be appreciated.







-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Computer Scientist
National Institute of Aerospace
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100726/6da706fe/attachment.htm>