--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on July 2010 ---
The first two questions have to do with \valid_range(...) the last is about CVC3(2.2). Question 1. ------------------ Alt-ergo can easily prove: /*@ assert m > 0 ; */ float *c = (float *) malloc(m *sizeof(float *)); /*@ assert \valid_range(c,0,(m-1)); */ but not /*@ assert m > 0 ; */ double *c = (double *) malloc(m *sizeof(double *)); /*@ assert \valid_range(c,0,(m-1)); */ I'm guessing this has to do with the size of doubles. Are there any hacks needed to make this work?? Question 2 ----------------- Suppose my C program has the format /* globally declaration */ struct Pstate{ int x; int y; int z[3]; }ps = { 0, 1, {0, 0, 0} } ; static void f(){ int i,j; int d; ..... d = ps.z[j]; ............. ps.z[i] = some other computation; } int main(int argc, char *argv[]) { /*@ assert \valid_range(ps.z,0,2);*/ ..... } It seems that such an assert should work since the array is initialized memory, but I seem to be wrong. What is the best way to get Jessie to recognize this ps.z[0..2] a valid memory range. Question 3. ------------------ Finally, I have installed CVC3 and frama-c recognizes it's there (at lest the GUI does) but all the calls seem to break. Is this just me or is some special switch needed for this one. Thanks for your help. -- Alwyn E. Goodloe 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/20100721/02c43ee0/attachment.htm>