--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on April 2013 ---
I'm trying to prove this contract holds (using Frama-C+Jessie) but can't find any annotation to make it work. Any ideas? /*@ @ terminates c>0; @ assigns \nothing; @*/ void f (int c) { /*@ @ loop assigns \nothing; @*/ while(!c) { } return; }