2021-01-26 19:14 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001071Frama-CPlug-in > Evapublic2012-01-26 10:022014-02-12 16:58
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon ftest.c (165 bytes) 2012-01-26 10:02 - 
    //@ requires 0 <= m <= n <= 9;
//  requires 0 <= m <= 9 && 0 <= n <= 9 && m <= n;
void main(int m,int n) {
    Frama_C_show_each_m(m);
    Frama_C_show_each_n(n);
}
    c file icon ftest.c (165 bytes) 2012-01-26 10:02 +

-Relationships
+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.
+Notes

-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
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
+Issue History