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] Unsound results from the value plugin on some arrays access

Hi Pierre,

On Fri, Apr 6, 2012 at 9:36 AM, Pierre Karpman
<Pierre.Karpman at rennes.supelec.fr> wrote:
> For instance, at some point in a program, I have a variable "i" which value
> is in {32, 64} (Frama-C computes this all right), and I also have an array
> "out" of size 64. Now if at this point I try to evaluate out[i], I get a
> result that's not bottom, which is quite troubling; but evaluating out[64]
> does yield a bottom result as I would expect. So it would seem that the
> knowledge of the value of "i" is not used when evaluating expressions where
> it appears? Is there any way to make it so?

I'm not sure there's a problem here. When you evaluate out[i], at
least one execution is possible: the one where i is equal to 32. Thus
it would be unsound to return Bottom, as the execution could possibly
continue. Conversely, at least one execution can lead to a runtime
error (if i is equal to 64). Thus, we emit an alarm saying that the
evaluation is possible only if i is such that 0 <= i < 64.

Depending on the version of Frama-C, and the way your code is written
(whether or not pointers are involved), Value may also reduce its
state when evaluating the remainder of the program. That is, since the
value 64 is guaranteed to lead to an error, it is correct to continue
the analysis with only the value 32 for i.

If you observe something different could you elaborate a bit on your
example, and provide us with a set of steps to reproduce in the Gui ?
Thanks !

Hope this helps,

-- 
Boris