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

  • Subject: [Frama-c-discuss] Unsound results from the value plugin on some arrays access
  • From: Pierre.Karpman at rennes.supelec.fr (Pierre Karpman)
  • Date: Fri, 06 Apr 2012 09:36:16 +0200
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]".