Frama-C Bug Tracking System - Frama-C
View Issue Details
0001071Frama-CPlug-in > Evapublic2012-01-26 10:022014-02-12 16:58
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001071: relation chains exploited incompletely
DescriptionRunning "frama-c -val ftest.c" on the attached program yields
"Called Frama_C_show_each_m([0..2147483647])
Called Frama_C_show_each_n([0..9])".
When the precondition in line 1 is replaced by the equivalent version in line 2, we obtain
"Called Frama_C_show_each_m([0..9])
Called Frama_C_show_each_n([0..9])".

Seemingly, from the relation chain "0 <= m <= n <= 9", the information "m <= 9" is not used.
TagsNo tags attached.
Attached Filesc ftest.c (165) 2012-01-26 10:02
https://bts.frama-c.com/file_download.php?file_id=327&type=bug

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.

Issue History
2012-01-26 10:02JochenNew Issue
2012-01-26 10:02JochenStatusnew => assigned
2012-01-26 10:02JochenAssigned To => pascal
2012-01-26 10:02JochenFile Added: ftest.c
2012-01-26 10:13pascalNote Added: 0002622
2012-01-27 14:04JochenNote Added: 0002629
2012-01-27 14:19pascalNote Added: 0002630
2012-01-27 15:55pascalNote Added: 0002631
2012-01-27 16:33svn
2012-01-27 16:33svnStatusassigned => resolved
2012-01-27 16:33svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:11pascalSource_changeset_attached => framac master f3027711
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon f3027711
2014-02-12 16:58pascalNote Added: 0004679
2014-02-12 16:58pascalStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva