do ... while{ } loop and -wp-invariants option
ID0002118: This issue was created automatically from Mantis Issue 2118. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002118 | Frama-C | Plug-in > wp | public | 2015-05-19 | 2015-06-29 |
| Reporter | blatterl | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Linux | OS | Fedora | OS Version | Version 17 |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
When I use the WP plug-in on the do ... while{ } loop below with the -wp-invariants option, WP proves all goals. But the ensures properties ("ensures n == 0 ==> \result == 0") of the function, including the do ... while{ } loop seems not valid to me. I get the same result if I replace the post condition "\result == 0" by anything. What is the exact semantics of the -wp-invariants option ?
/@ ensures n == 0 ==> \result == 0; / int fonction(int n, int a){ int i = 0; int b = 0; /@ loop invariant b == ia; / do { b = b+a; i = i+1; } while (i < n); /@ assert n== 0 ==> b==a; */ return b; }
Steps To Reproduce :
frama-c -wp -wp-invariants file.c with file.c containing the above snippet.