--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on January 2010 ---
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