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] A variation domain failed to be computed

  • Subject: [Frama-c-discuss] A variation domain failed to be computed
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Wed, 6 May 2009 19:25:00 +0200
  • References: <1241624519.21376.229.camel@supelec>
> Here is a small code sample:

Although it is clear that you are using the option -lib-entry,
please include the command-line when discussing the precise behavior
of the analysis on an example.

>Apparently when assigning
>'ret' to 'pw->pw_passwd[0]' it forgots that 'pw->pw_passwd[0]' should be
>'0' in that codeblock and fallback to 'alloced_return_getpwnam'.

The indirection ->, and the fact that the superset for
the values of pw contains more than one valid pointer,
are the causes for this imprecision.
Actually there is a mechanism in place for trying to
remember that *p is 0 even when p may point to
several different locations in memory, but this mechanism
is resource-consuming and all the information of this nature
is forgotten at function calls and function returns (and there are
other technical limitations that can prevent this mechanism to
work. You should not count on it, just consider it a
"precision bonus" when it works).

>So I was wondering if it's should be reported as a bug or if it's the
>intended behavior.

It is the intended behavior, kindof. The implications of memorizing
the kind of information that you need here would make the
analysis worse, not better. One thing that you can do is
insert an ACSL assertion to describe the property that you would like to
hold in the then branch. The value analysis may use the assertion, and
it would be very likely to be discharged by a weakest precondition
plug-in. Of couse, this is only a work-around, not a perfect solution.

> Because If I use a temporary variable, I can get the
>correct variation domain:

It's easier in this case because there is no indirection.
tmp is obviously a single location in memory.

>Also I was wondering if there is way to make the value analysis plugin
>provides only 'real value' variation domains.
>I'm not sure how to say this properly so as an example, in the code
>sample following this sentence, the value analysis plugin would give me
>of course {0; } for the variation domain of 'ret' in 'code 1', but would
>also give me [1..255] (the whole range of possible values minus '0') in
>'code 2' instead of 'alloced_return_getpwnam'.

No, and in a funny way it's for the same reason: The analyzer has several
representations for the same value. It knows that 0 is a representation
of zero and it knows that &alloced_return_getpwnam+555555, an invalid
address, may happen to be zero too,
but it does not want to make an hypothesis on
whether these two are the same or different. Because of this "aliasing"
between the representation of values, when you substract {0} from the
set of possible values for ret, it's not possible to be exact. So it's
not possible to infer that 0 is not in the resulting, reduced set.

Pascal