2021-03-01 04:57 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000733Frama-CPlug-in > inoutpublic2011-02-20 19:162017-05-31 19:05
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C 15-Phosphorus 
Summary0000733: Invalid results in presence of pseudo-recursive calls in inout and from
DescriptionThe Inout and From plugins are apparently designed to handle "pseudo" recursive calls, ie. when the value analysis does not detect a recursive call, but the plugin see a circularity in the stacks of examined functions. However, they are all buggy, because of the way the results are cached.

Indeed, when a circularity is encountered, the analysis is stopped immediately. This means that the results for the first function in the cycle is correct, but not those for the intermediate functions.

This can be seen with the example file: the inputs (option -input) for function h2 should include x.
Additional InformationCommit 12050 has removed most of the warnings the plugins printed unnecessarily when those pseudo recursive calls were encountered, so the error can now be completely silent (however, even with the warnings the plugins were buggy, as they implied that the analysis was correct if the value analysis was happy).

I have some (quite obvious) suggestions for correcting the bug, but they are not very efficient wrt to time complexity. Suggestions are welcome.
TagsNo tags attached.
Attached Files
  • ? file icon recursion2.i (239 bytes) 2011-02-20 19:16 - 
    /*run.config
  OPT: -journal-disable -input -val
 */
int x, y;

void h2 (int);
void h1 (int);

void h1 (int i) {
  int r = x;
  if (i)
    h2 (i);
}
void h2 (int i) {
  int r = y;
  if (!i)
    h1 (i);
}

void main() {
  h2(0);
  h1(1);
}
    ? file icon recursion2.i (239 bytes) 2011-02-20 19:16 +

-Relationships
+Relationships

-Notes

~0001527

pascal (reporter)

2011-02-20 21:09

 1/ I know.

2/ From my point of view any sort of recursion (that is, any cycle in the syntactic call graph) is unsupported in the value analysis and derived analyses. Perhaps I should assign the bug to you so that you feel free to do what's necessary (as long as you don't break what works for programs without recursion)?

~0001671

yakobowski (manager)

2011-03-31 21:59

 Bug remains in From and Operation_inputs plugins.

~0006391

yakobowski (manager)

2017-03-31 20:17

 No longer relevant in Phosphorus, where -inout-callwise is set by default.
+Notes

-Issue History
Date Modified Username Field Change
2011-02-20 19:16 yakobowski New Issue
2011-02-20 19:16 yakobowski Status new => assigned
2011-02-20 19:16 yakobowski Assigned To => pascal
2011-02-20 19:16 yakobowski File Added: recursion2.i
2011-02-20 21:09 pascal Note Added: 0001527
2011-02-22 01:08 yakobowski Assigned To pascal => yakobowski
2011-02-23 11:00 svn
2011-03-31 21:59 yakobowski Note Added: 0001671
2011-03-31 21:59 yakobowski Status assigned => acknowledged
2013-06-11 23:10 yakobowski Severity major => minor
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master 9cee84b1
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 9cee84b1
2017-03-31 20:17 yakobowski Note Added: 0006391
2017-03-31 20:17 yakobowski Status acknowledged => resolved
2017-03-31 20:17 yakobowski Resolution open => fixed
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
+Issue History