--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Inout analysis question



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>