| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000733 | Frama-C | Plug-in > inout | public | 2011-02-20 19:16 | 2017-05-31 19:05 |
|
| Reporter | yakobowski | |
| Assigned To | yakobowski | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Carbon-20110201 | |
| Target Version | | Fixed in Version | Frama-C 15-Phosphorus | |
|
| Summary | 0000733: Invalid results in presence of pseudo-recursive calls in inout and from |
| Description | The 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 Information | Commit 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. |
| Tags | No tags attached. |
|
| Attached Files |  recursion2.i [^] (239 bytes) 2011-02-20 19:16 [Show Content] [Hide Content]/*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);
}
|
|
Relationships 
Relationships