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] approximations in value analysis

On Thursday, July 7, 2011, SENE, Sali <sali.sene at airbus.com> wrote:

> I have many approximations in the result of my analysis. Some of this approximations are caused by arithmetic on variable pointer.

Be aware that the indications provided in the log are only hints as to
the cause of the approximation. Engineer judgement is required to
determine, with help from these hints, the true cause of the
approximation.
>
> sources/alloc_new.c:59:[value] reading left-value new.
> ??????? It contains a garbled mix of {heap; ioctl_requests; ioctl_args; "DRIVER DSO"; }
> ??????? because of Arithmetic {sources/alloc_new.c:56; }.
>
> The line alloc_new.c:56
> new->size = (int)next - (int)new - BLOCK_SIZE;
>
> next and new are some variable pointer.

This is something that the value analysis handles perfectly, as you
can check on a small example, when next and new are in the same block.
It cannot handle it (because there is no good answer) when it has not
been able to determine that next and new point inside the same block.
If this is the reason for the approximation, the fix is to force the
value analysis to reach this line only with values for next and new
inside the same block, by whatever means.

Pascal