[Frama-c-discuss] annotations and value analysis

Stéphane Duprat stephane.duprat at atosorigin.com
Thu Jan 21 12:34:11 CET 2010


I have some questions about the use of annotations in the value analysis
of Frama-c.
First, I know that value analysis doesn't handle all annotations for
different reasons (for ex. requires \valid(p+10) and I exclude theses
annotations for this subject.
Here is a small stub function :

          @ requires 0<=cmd<5;
          @ ensures  0<=\result<200;
        int get_index(int /* in */ cmd)
          int v = cmd;
          int ret = (unsigned int)Frama_C_interval(0,1000);
          return ret;

My questions are :
  1/ does requires are checked by the value analysis considering the
calling context ?
  2/ does requires are hypothesis for the body of the function ?
  3/ does the ensures are checked by the value analysis ?
  4/ does the ensures of a called function are taken into account for
the analysis of the caller ?
Using the tool, I would answer yes for all except for 4/. But I prefer
asking you.

Ensures could be usefull to define a minimal semantic for function with
just a declaration (and without any definition of stub).

thx a lot,


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100121/50e2cc94/attachment.htm 

More information about the Frama-c-discuss mailing list