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

>> new->size = (int)next - (int)new - BLOCK_SIZE;
> 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.

Actually, it occurs to me that we could emit an alarm stating that
next and new *must* be in the same block for the subtraction to make
sense, and then evaluate the result as the set of values that can be
obtained under this condition. This would save user time for this
example, but only if the program never subtracts two pointers to
different blocks on purpose. If the program did this on purpose, this
would make it impossible to analyze.

Pascal