[Frama-c-discuss] annotations and value analysis
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
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);
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
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...
More information about the Frama-c-discuss