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.