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



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]".