Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #339
Closed
Open
Issue created Feb 20, 2011 by Boris Yakobowski@byakoDeveloper

Invalid results in presence of pseudo-recursive calls in inout and from

ID0000733: This issue was created automatically from Mantis Issue 733. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000733 Frama-C Plug-in > inout public 2011-02-20 2017-05-31
Reporter yakobowski Assigned To yakobowski Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20110201 Target Version - Fixed in Version Frama-C 15-Phosphorus

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.

Attachments

  • recursion2.i
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking