# 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] Issue understanding Value analysis approximation on loop bounds

*Subject*: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds*From*: boris at yakobowski.org (Boris Yakobowski)*Date*: Sat, 28 Apr 2012 13:45:20 +0200*In-reply-to*: <CAC3Lx=YsN9UReq035Y93i0pyo0TGYWmV4uK+u+wccvN-thDVLg@mail.gmail.com>*References*: <CAC3Lx=YsN9UReq035Y93i0pyo0TGYWmV4uK+u+wccvN-thDVLg@mail.gmail.com>

Hi David, Here are a few complements to the answer that was given on the blog. I think there exists a very common misunderstanding concerning the action of option -slevel k. What it does _not_ do is unroll loops k times. In many cases, this is what seems to happen. However, the real effect is to allow the independent propagation of k different states, for each statement. For simple loops, this is equivalent, as you need one state per value of the loop index. In other cases, it is clearly not: #define N 10 int t[N]; volatile int v; void main() { for (int i=0;i<N;i++) { if (v) t[i] = i; } } This example needs an slevel of 256 to be unrolled completely, because Value ultimately propagates all (t[1] ? {0, 1}) x ... x (t[9] ? {0, 9}) combinations. This is not useful here (the values of t[i-m] are not useful to compute t[i]), but this fact is not obvious without some prior analysis, which would have to influence the propagation strategy of Value. As an additional example, your code within #ifdef ADDITIONAL_IF double the number of slevel required, because two states for 'a' are propagated separately. Does this explain your last interrogation (more than 10000 slevel required)? Next, once you have more than one loop, things get much more complicated. With your nested loops, the -slevel 100 you chose is insufficient to propagate all possible states. So a question of fairness appears: should some fraction of the slevel be used for the inner loop, and the remainder for the outer one? Or should all the slevel be consumed by one of the two loops? But this is in fact a rhetorical question. As Pascal wrote, Value has a low-level view of the control-flow-graph, in which notions of inner and outer loops are almost meaningless. The order in which Value propagates states is thus entirely unspecified. For code such as yours, the "good" solution is to use enough slevel to entirely unroll the loops, or almost none at all. In your example, using a slevel of 2 or of 100 does little difference. I can however shed another light on why adding some statements degrade the precision on k. In your example, the new statement changes not only the propagation strategy, but also increases the number of widening steps that are performed. Here, more widening are performed on the inner loop, and j ends up being widened there [1]. This can for example be observed in the gui [2]. This is turn degrades the precision on k, but the real cause is the loss of precision on j. My suggestion to avoid this would be to add another loop invariant on j, this time to the inner loop. /*@ loop invariant min <= j < max; loop invariant j - 31/2 <= k && k <= j+31/2+1; */ Hope this clear things up, [1] The current approach for finding which variables should be widened could be made a bit smarter. For example, there is no real reason to widen j in the inner loop, as it is not increased within. Conversely, k should not be widened in the outer loop. The second possibility does not occur here (I think), but the first one does. However, this is complicated to get right without endangering the convergence of the analysis in corner cases. [2] The loss of precision on j is not visible in the synthetic text results. The possible values for j are constrained by your loop invariant each time the outer "loop" statement is analyzed. At some point, when j is widened to 127 by the inner loop, the loop invariant gets status unknown. However, the range of j keeps getting constrained at the beginning of the loop body. You may have detected this by using Frama_C_show_each_k_j(k, k); in your inner loop, but sing the GUI to see the possible ranges of important variables at various statements is complementary to the use of Frama_C_show_each(). Notice that, with the additional loop invariant on j, both invariant related to j get status Valid. -- Boris

**References**:**[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds***From:*dmentre at linux-france.org (David MENTRE)

- Prev by Date:
**[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds** - Previous by thread:
**[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds** - Index(es):