--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on July 2010 ---
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>