--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on January 2010 ---
> I guess it will be same with output parameters of the function > (gest_index(int cmd, int* pindex). Can you confirm ? If you mean adding respectively: @ ensures *p >= 10 ; ... int get_index(int /* in */ cmd, int *p) ... get_index(x, &R); It is already supported: [value] Values for function main: R ? [10..199] > And what about annotation on declaration of the function without > definition? In this case you *need* an assigns clause in the function contract. You can use dependencies (\from ...), the extension described at page 56 of the currently distributed ACSL documentation. The assigns clause with dependencies is interpreted by the value analysis, but at this time, the pre- and post-conditions are not. The policy is that announcement of features and dates is not allowed on this mailing-list (as per http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-November/000780.html ) and therefore, since I would never go against one of this mailing list's official policy, I can't have promised support for \result soon. Similarly I can't comment on the availability of support for pre- and post-conditions in library function specifications in the value analysis. Pascal -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100121/fc498cd6/attachment.htm