|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001071||Frama-C||Plug-in > Eva||public||2012-01-26 10:02||2014-02-12 16:58|
|Product Version||Frama-C Nitrogen-20111001|
|Target Version||Fixed in Version||Frama-C Oxygen-20120901|
|Summary||0001071: relation chains exploited incompletely|
|Description||Running "frama-c -val ftest.c" on the attached program yields|
When the precondition in line 1 is replaced by the equivalent version in line 2, we obtain
Seemingly, from the relation chain "0 <= m <= n <= 9", the information "m <= 9" is not used.
|Tags||No tags attached.|
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.
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.)
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
|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.|
|Fix committed to stable/neon branch.|
|2012-01-26 10:02||Jochen||New Issue|
|2012-01-26 10:02||Jochen||Status||new => assigned|
|2012-01-26 10:02||Jochen||Assigned To||=> pascal|
|2012-01-26 10:02||Jochen||File Added: ftest.c|
|2012-01-26 10:13||pascal||Note Added: 0002622|
|2012-01-27 14:04||Jochen||Note Added: 0002629|
|2012-01-27 14:19||pascal||Note Added: 0002630|
|2012-01-27 15:55||pascal||Note Added: 0002631|
|2012-01-27 16:33||svn||Status||assigned => resolved|
|2012-01-27 16:33||svn||Resolution||open => fixed|
|2012-09-19 17:15||signoles||Fixed in Version||=> Frama-C Oxygen-20120901|
|2012-09-19 17:16||signoles||Status||resolved => closed|
|2013-12-19 01:11||pascal||Source_changeset_attached||=> framac master f3027711|
|2014-02-12 16:54||pascal||Source_changeset_attached||=> framac stable/neon f3027711|
|2014-02-12 16:58||pascal||Note Added: 0004679|
|2014-02-12 16:58||pascal||Status||closed => resolved|
|2018-01-12 14:26||signoles||Category||Plug-in > value analysis => Plug-in > Eva|