Notes 

(0002622)

pascal

20120126 10:13


0 <= m <= n <= 9 is syntactic sugar for 0 <= m && m <= n && n <= 9
The value analysis is nonrelational and interprets the assertions lefttoright.
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 ABA pattern when interpreting A && B,
but this comes at an additional cost (also note that there is no reason why ABA 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

20120127 14:04


I would be happy with the recommended "simple fix".
(Nevertheless I'd be curious about an example of arbitrarily many iterations ABAB..., if one is available.) 


(0002630)

pascal

20120127 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

20120127 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

20140212 16:58


Fix committed to stable/neon branch. 
