--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on January 2010 ---
Hi, 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, St?phane -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100121/50e2cc94/attachment.htm