--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2012 ---
Hello, I'm using the value analysis of Frama-C, and it sometimes gives me results that I don't completely understand; I'm not quite sure if it is a problem from the plugin itself, or merely from how I'm using it. 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? Cheers, Pierre P.S. I first encountered this behaviour while using a plugin that intercepts the results of the value analysis at various points in the analysed programs; I then reproduced it whit the GUI to compare the results for say "out[i]" and "out[64]".