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

[Frama-c-discuss] annotations and value analysis



Hello, St?phane,

>   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/.

In fact, it is "yes" for all 4 in the development version
of Frama-C. On the other hand, the value analysis
does not yet support \result in post-conditions.

Changing your example thus:

int R;

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

void main(x)
{
   get_index(x);
   return R;
}

you get:

[value] Values for function main:
           R ? [0..199]

Part of the restructuration necessary to handle \result
in post-conditions has already been done, but it is
not complete at this time.

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100121/503c4b6c/attachment.htm