--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on February 2012 ---
Hi, I have some doubts about wp. A simple program named b.c as below void phase(void) { int m; int a; m = 0; a = 10; /*@ loop invariant a-10 == 0; loop invariant m >= 0; */ while(m<=a) { m=m+1; } return; } void main(void) { phase(); return; } There are two invariants here. Now run the command "frama-c-gui b.c" and we can find that both of the status of the invariants is "no verification attempted". If I click the menu "Prove the annotation by WP" on one of them and get the result is local status--valid consolidated status--unkonwn. Then click the menu on the other invariant and the statuses all become to be valid. If wp is dynamically called with code to prove the invariants it can only be proved one by one. How to get the "VALID" results above? ---- Best regards. Henry -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120215/1261861c/attachment.htm>