Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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 file icon ftest.c [^] (165 bytes) 2012-01-26 10:02 [Show Content]

- Relationships

-  Notes
(0002622)
pascal (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
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 Checkin
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
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker