Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #2054

loop invariant cannot conclude (due to an assertion)

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


Id Project Category View Due Date Updated
ID0001172 Frama-C Kernel > ACSL implementation public 2012-04-23 2012-04-23
Reporter nmuller Assigned To virgile Resolution no change required
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version -

Description :

<<< abs_new_1.c >>> The previous verison, "abs_new.c" code had some minor problems with the annotations, that it was not able to validate two assertions, when used using Jessie, but the code was changed and analysed using "WP", we found out that we again had some problems, this time it was only one assertion in the last part of the program at "line:59", which was not getting validated, rest of the other assertions of the same type were getting validated in the previous loops, so we inserted a "loop invariant for the same assertion" without removing the existing unknown assertion and we tried to prove it by Wp , interestingly this time the assertion was validated but the loop invariant corresponding to the assertion was "time out" (although the time out has been increased up to 200).

Quite interesting indeed, as we are not that strong in the underlying theory of the WP analyser, but to our understanding on looking on to the prolem,we feel that the an assertion for any line of C code inside a loop should be declared as a loop invariant, so that it goes around like in a circle, first it validates the assertion and comes back to the loop invariant in order to be valid, but in our case the once the assertion is valid, its not able to retrace back to the loop invariant to validate it, and so the loop invariant becomes "time out".

Attachments

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