Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] valid range of arrays within structures
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Mon, 26 Jul 2010 15:03:53 -0400
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>