--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on April 2012 ---
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