Skip to content

GitLab

  • Menu
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 201
    • Issues 201
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & 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
  • #569
Closed
Open
Created Dec 03, 2015 by mantis-gitlab-migration@mantis-gitlab-migration

WP output of loop variant's goal doesn't have location of loop variant

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


Id Project Category View Due Date Updated
ID0002190 Frama-C Plug-in > wp public 2015-12-03 2016-01-26
Reporter gaggarwal Assigned To correnson Resolution won't fix
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Sodium Target Version - Fixed in Version -

Description :

Consider the following example:

  1. void main() {
  2. int i;
  3. /*@ loop invariant 0 <= i <= 5;
  4.   @ loop variant 5-i;
  5.   @*/
  6. for(i=0;i<5;i++);
  7. }

Output generated by wp for loop variant is following:

Goal Decreasing of Loop variant at loop (file /SpecDemo/src/test6.c, line 6): Assume { (* Domain *)
...... Prove: true. Prover Qed returns Valid

Goal Positivity of Loop variant at loop (file /SpecDemo/src/test6.c, line 6): Assume { (* Domain *) ....... Prove: true. Prover Qed returns Valid

Notice that both goals have location of loop i.e. (file /SpecDemo/src/test6.c, line 6) and not of loop variant. Even though a loop can have only one loop variant and it is not very hard to figure out which loop variant it is, it will be really helpful if we can include location of loop variant too.

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