|
Notes |
|
|
(0002622)
|
|
pascal
|
|
2012-01-26 10:13
|
|
0 <= m <= n <= 9 is syntactic sugar for 0 <= m && m <= n && n <= 9
The value analysis is non-relational and interprets the assertions left-to-right.
Therefore, it cannot take advantage of property m <= n when it sees it, because n has not been constrained yet when it sees it.
This could be fixed by following an A-B-A pattern when interpreting A && B,
but this comes at an additional cost (also note that there is no reason why A-B-A would be enough. In theory, alternately reducing with A and with B may be a case of slow convergence for which you would need arbitrarily many iterations to reach the optimal result).
The desugared form may also be recognized as a special pattern and optimized. This is the simple fix that I would recommend. |
|
|
|
(0002629)
|
|
Jochen
|
|
2012-01-27 14:04
|
|
I would be happy with the recommended "simple fix".
(Nevertheless I'd be curious about an example of arbitrarily many iterations A-B-A-B-..., if one is available.) |
|
|
|
(0002630)
|
|
pascal
|
|
2012-01-27 14:19
|
|
The following assertion, starting with 0 <= x <= 1000 and 0 <= y <= 1000, will go through 1000 iterations of reducing for A — x >= y and B — y < x before eventually concluding that the solution set is empty.
Stopping at any time before the 1000 iterations yield a result that is correct, improved with respect to the initial state and all previous iterations, but not optimal.
assert x >= y && y < x |
|
|
|
(0002631)
|
|
pascal
|
|
2012-01-27 15:55
|
|
|
Note that you can write Frama_C_show_each_mn(m, n);. It is shorter. When using -slevel, it also shows more clearly what values for m are propagated with which values of n. |
|
|
|
(0004679)
|
|
pascal
|
|
2014-02-12 16:58
|
|
|
Fix committed to stable/neon branch. |
|
ftest.c (165) 2012-01-26 10:02