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] three newbie questions

  • Subject: [Frama-c-discuss] three newbie questions
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Wed, 21 Jul 2010 14:25:42 -0400
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>