Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>