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

[Frama-c-discuss] three newbie questions



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>