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

Hello,
> Hi Pierre,
>
> On Fri, Apr 6, 2012 at 9:36 AM, Pierre Karpman
> <Pierre.Karpman at rennes.supelec.fr  <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>>  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.
I see your point. So I think my problem comes from the fact that I'm 
considering the values for variables at points where they may not be 
used in the source. That is, given the simple example:
int main (int argc, char **argv)
{
     int arr[2]; int i;

      arr[0] = 0; arr[1] = 1;
      if (argc % 2)
          i = 0;
      else
          i = 72;
      return 0; //mark1
}
although arr[i] is not used at mark1, I'd still like to know what the 
value analysis can say about it. This can be done e.g. in the GUI by 
asking to evaluate the expression "arr[i]" at this statement, which will 
give me the result "arr[i] == 0"; this is confusing because the right 
way to interpret the result would be "if this expression were to be in 
the source; if the program didn't fail, then it would have this value", 
but there isn't any hint about which conditions are necessary for the 
program not to pretend-fail when we pretend-evaluate it, as there would 
be in the form of an assert statement if the expression was actually in 
the source.
I will probably add the checks I need in my code, then.

Cheers,
Pierre

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120406/8310821b/attachment.html>