--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on February 2011 ---
Hello Victoria, > [inout] done for function main > [inout] InOut (with formals) for function main: > Operational inputs: taille > Operational inputs on termination: taille > Sure outputs: *S_taille*[0] > [inout] Inputs (with formals) for function main: > taille; *S_taille*[0] > > where our formal parameter is considered as an imperative input but not an > operational one. > This is correct and optimal. > If we replace the first if clause by the second one : > > > [inout] InOut (with formals) for function main: > Operational inputs: taille; *S_taille*[0] > Operational inputs on termination: taille; *S_taille*[0] > Sure outputs: *S_taille*[0] > [inout] Inputs (with formals) for function main: > taille; *S_taille*[0] > > In this last case, the formal parameter is considered as an operational > input as well as an imperative one. > > This is correct and over-approximated. The operational inputs analysis could omit S_taille[0] but it does not realize that it can. The imprecision is in the handling of function calls. I will see if the analysis' precision can be improved on your example. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110217/12199e7b/attachment.htm>